(* File: NSearch.v  (last edited on 27/10/2000) (c) Klaus Weich  *)


Require Export Disjunct.
Require Export NWeight.
Require Export Lt_Ks.
Require Export NRules.


Definition nsearch_invariant (n : nat) :=
  forall (goal : Int) (work : nf_list) (ds : disjs) 
    (ni : nested_imps) (ai : atomic_imps) (a : atoms) 
    (context : flist),
  nweight_Sequent work ds ni ai < n ->
  REGULAR normal_form ai ->
  a_ai_disj a ai ->
  a_goal_disj a goal -> nsearch_spec goal work ds ni ai a context.



Lemma nsearch_aux : forall n : nat, nsearch_invariant n.

(* Goal: forall n : nat, nsearch_invariant n *)
intros n; elim n; clear n.
(* n=0 *)
(* Goal: nsearch_invariant (S n) *)
unfold nsearch_invariant in |- *.
(* Goal: forall (goal : Int) (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (context : flist) (_ : lt (nweight_Sequent work ds ni ai) O) (_ : REGULAR normal_form ai) (_ : a_ai_disj a ai) (_ : a_goal_disj a goal), nsearch_spec goal work ds ni ai a context *)
(* Goal: forall (n : nat) (_ : nsearch_invariant n), nsearch_invariant (S n) *)
intros goal work ds ni ai a context lt_nweight ai_reg a_ai_disj a_goal_disj.
(* Goal: nsearch_spec goal work ds ni ai a context *)
(* Goal: forall (n : nat) (_ : nsearch_invariant n), nsearch_invariant (S n) *)
elimtype False.
(* Goal: False *)
(* Goal: forall (n : nat) (_ : nsearch_invariant n), nsearch_invariant (S n) *)
apply (lt_n_O (nweight_Sequent work ds ni ai)); assumption.

(* n>0 *)
(* Goal: forall (n : nat) (_ : nsearch_invariant n), nsearch_invariant (S n) *)
intros n ih_n.
(* Goal: nsearch_invariant (S n) *)
unfold nsearch_invariant in |- *.
(* Goal: forall (goal : Int) (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (context : flist) (_ : lt (nweight_Sequent work ds ni ai) (S n)) (_ : REGULAR normal_form ai) (_ : a_ai_disj a ai) (_ : a_goal_disj a goal), nsearch_spec goal work ds ni ai a context *)
intros goal work ds ni ai a.
(* Goal: forall (context : flist) (_ : lt (nweight_Sequent work ds ni ai) (S n)) (_ : REGULAR normal_form ai) (_ : a_ai_disj a ai) (_ : a_goal_disj a goal), nsearch_spec goal work ds ni ai a context *)
elim ai; clear ai.
(* Goal: forall (t : avl_tree nf_list) (i : is_avl nf_list t) (context : flist) (_ : lt (nweight_Sequent work ds ni (AVL_intro nf_list t i)) (S n)) (_ : REGULAR normal_form (AVL_intro nf_list t i)) (_ : a_ai_disj a (AVL_intro nf_list t i)) (_ : a_goal_disj a goal), nsearch_spec goal work ds ni (AVL_intro nf_list t i) a context *)
intros ai avl_ai.
(* Goal: forall (context : flist) (_ : lt (nweight_Sequent work ds ni (AVL_intro nf_list ai avl_ai)) (S n)) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_ai_disj a (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj a goal), nsearch_spec goal work ds ni (AVL_intro nf_list ai avl_ai) a context *)
elim a; clear a.
(* Goal: forall (t : avl_tree unit) (i : is_avl unit t) (context : flist) (_ : lt (nweight_Sequent work ds ni (AVL_intro nf_list ai avl_ai)) (S n)) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_ai_disj (AVL_intro unit t i) (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit t i) goal), nsearch_spec goal work ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit t i) context *)
intros a avl_a.
(* Goal: forall (context : flist) (_ : lt (nweight_Sequent work ds ni (AVL_intro nf_list ai avl_ai)) (S n)) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal), nsearch_spec goal work ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros context lt_nweight ai_reg a_ai_disj a_goal_disj.
generalize ds ni ai avl_ai a avl_a ai_reg a_goal_disj a_ai_disj lt_nweight;
 clear lt_nweight ai_reg a_ai_disj a_goal_disj avl_ai avl_a ds ni ai a.

(* Goal: forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent work ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal work ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
elim work; clear work.
(* work=nf_nil *)
(* Goal: forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@nil normal_form) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@nil normal_form) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
fold nf_nil in |- *.
(* Goal: forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
intros ds; case ds; clear ds.
(* ds=nil *)
(* Goal: forall (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@nil disj) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@nil disj) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
fold DNil in |- *.
(* Goal: forall (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil DNil ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
intros ni ai avl_ai a avl_a ai_reg a_goal_disj a_ai_disj.
(* Goal: forall _ : lt (nweight_Sequent nf_nil DNil ni (AVL_intro nf_list ai avl_ai)) (S n), nsearch_spec goal nf_nil DNil ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
pattern ni in |- *.
(* Goal: (fun n0 : nested_imps => forall _ : lt (nweight_Sequent nf_nil DNil n0 (AVL_intro nf_list ai avl_ai)) (S n), nsearch_spec goal nf_nil DNil n0 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) ni *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply My_Lt_Ks_rec; clear ni.
(* Goal: forall (ni2 : nested_imps) (dni2 : decorated_nested_imps) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 ni2 dni2) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni2 ni2) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni2 ni2) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
intros ni dni.
(* Goal: forall (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 ni dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni ni) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni ni) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
case ni; clear ni.
(* Goal: forall (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@nil nested_imp) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@nil nested_imp)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@nil nested_imp)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nested_imp) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp n0 l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp n0 l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp n0 l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
fold NNil in |- *.
(* Goal: forall (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 NNil dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni NNil) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni NNil) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nested_imp) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp n0 l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp n0 l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp n0 l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
intros ih lt_nweight.
(* Goal: nsearch_spec goal nf_nil DNil (rev_app dni NNil) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nested_imp) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp n0 l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp n0 l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp n0 l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply fail; assumption.
(* ni'=  *)
(* Goal: forall (n0 : nimp) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Undecorated n0) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Undecorated n0) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Undecorated n0) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
intros x; case x; clear x.
(* Goal: forall (n0 : nimp) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Undecorated n0) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Undecorated n0) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Undecorated n0) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
intros x; case x; clear x.
(* Goal: forall (i i0 : Int) (n0 : normal_form) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Undecorated (NImp i i0 n0)) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Undecorated (NImp i i0 n0)) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Undecorated (NImp i i0 n0)) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
intros a0 a1 b ni ih lt_nweight.
(* Goal: nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Undecorated (NImp a0 a1 b)) ni)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply left_nimp; try assumption.

(* Goal: forall (ni1 : nested_imps) (_ : le_ni ni1 (rev_app dni ni)), nsearch_spec goal (@cons normal_form b nf_nil) DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (ni1 : nested_imps) (k : kripke_tree) (_ : le_ni ni1 (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree (NImp a0 a1 b) k) dni) ni)), nsearch_spec goal nf_nil DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
intros ni1 le1; clear ih.
(* Goal: nsearch_spec a1 (@cons normal_form (AImp a1 b) (@cons normal_form (NAtom a0) nf_nil)) DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) (@cons form (Atom a0) context) *)
(* Goal: forall (ni1 : nested_imps) (_ : le_ni ni1 (rev_app dni ni)), nsearch_spec goal (@cons normal_form b nf_nil) DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (ni1 : nested_imps) (k : kripke_tree) (_ : le_ni ni1 (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree (NImp a0 a1 b) k) dni) ni)), nsearch_spec goal nf_nil DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
elim (lookup_dec unit a1 a avl_a).
(* Goal: forall (d : unit) (_ : lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros d; case d; clear d.
(* Goal: forall _ : lookup unit i a tt, nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros lookup.
(* Goal: nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : not (Equal goal i), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply nax; try assumption.
(* Goal: in_ngamma (@cons normal_form (AImp a1 b) (@cons normal_form (NAtom a0) nf_nil)) DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) (NAtom a1) *)
(* Goal: forall _ : forall d : unit, not (lookup unit a1 a d), nsearch_spec a1 (@cons normal_form (AImp a1 b) (@cons normal_form (NAtom a0) nf_nil)) DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) (@cons form (Atom a0) context) *)
(* Goal: forall (ni1 : nested_imps) (_ : le_ni ni1 (rev_app dni ni)), nsearch_spec goal (@cons normal_form b nf_nil) DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (ni1 : nested_imps) (k : kripke_tree) (_ : le_ni ni1 (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree (NImp a0 a1 b) k) dni) ni)), nsearch_spec goal nf_nil DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply In_Atoms; assumption.
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros not_lookup.
(* Goal: nsearch_spec goal (@app normal_form bs work) ds ni (AVL_intro nf_list ai' avl_ai') (AVL_intro unit a' avl_a') context *)
(* Goal: forall _ : forall d : nf_list, not (lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply ih_n; try assumption.
(* Goal: lt (nweight_Sequent (@cons normal_form (AImp a1 b) (@cons normal_form (NAtom a0) nf_nil)) DNil ni1 (AVL_intro nf_list ai avl_ai)) n *)
(* Goal: Disjunct.a_goal_disj (AVL_intro unit a avl_a) a1 *)
(* Goal: forall (ni1 : nested_imps) (_ : le_ni ni1 (rev_app dni ni)), nsearch_spec goal (@cons normal_form b nf_nil) DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (ni1 : nested_imps) (k : kripke_tree) (_ : le_ni ni1 (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree (NImp a0 a1 b) k) dni) ni)), nsearch_spec goal nf_nil DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply nweight_sequent_nimp_left with ni dni; try assumption.
(* Goal: eqv_ni ni ni1 *)
(* Goal: lt (nweight_Sequent nf_nil (@cons (prod Int Int) (@pair Int Int i j) ds) ni (AVL_intro nf_list ai avl_ai)) (S n) *)
(* Goal: forall (ni2 : nested_imps) (_ : eqv_ni ni2 ni), nsearch_spec goal (@cons normal_form (NAtom j) nf_nil) ds ni2 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) (@cons form (Atom j) context) *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply le_eqv; assumption.
(* Goal: Disjunct.a_goal_disj (AVL_intro unit a avl_a) a1 *)
(* Goal: forall (ni1 : nested_imps) (_ : le_ni ni1 (rev_app dni ni)), nsearch_spec goal (@cons normal_form b nf_nil) DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (ni1 : nested_imps) (k : kripke_tree) (_ : le_ni ni1 (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree (NImp a0 a1 b) k) dni) ni)), nsearch_spec goal nf_nil DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
exact (not_lookup tt).

(* Goal: forall (ni1 : nested_imps) (_ : le_ni ni1 (rev_app dni ni)), nsearch_spec goal (@cons normal_form b nf_nil) DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (ni1 : nested_imps) (k : kripke_tree) (_ : le_ni ni1 (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree (NImp a0 a1 b) k) dni) ni)), nsearch_spec goal nf_nil DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
intros ni1 le1; clear ih.
(* Goal: nsearch_spec goal (@app normal_form bs work) ds ni (AVL_intro nf_list ai' avl_ai') (AVL_intro unit a' avl_a') context *)
(* Goal: forall _ : forall d : nf_list, not (lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply ih_n; try assumption.
(* Goal: lt (nweight_Sequent (@cons normal_form b nf_nil) DNil ni1 (AVL_intro nf_list ai avl_ai)) n *)
(* Goal: forall (ni1 : nested_imps) (k : kripke_tree) (_ : le_ni ni1 (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree (NImp a0 a1 b) k) dni) ni)), nsearch_spec goal nf_nil DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply nweight_sequent_nimp_right with a0 a1 ni dni; try assumption.
(* Goal: eqv_ni (rev_app dni ni) ni1 *)
(* Goal: forall (ni1 : nested_imps) (k : kripke_tree) (_ : le_ni ni1 (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree (NImp a0 a1 b) k) dni) ni)), nsearch_spec goal nf_nil DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply ge_eqv; assumption.

(* Goal: forall (ni1 : nested_imps) (k : kripke_tree) (_ : le_ni ni1 (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree (NImp a0 a1 b) k) dni) ni)), nsearch_spec goal nf_nil DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
intros ni1 k le1.
(* Goal: nsearch_spec goal nf_nil DNil ni1 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply ih with (ni1 := ni1) (dni1 := DNI_NIL); clear ih; try assumption.
(* Goal: Lt_Ks ni1 DNI_NIL (@cons nested_imp (Undecorated (NImp a0 a1 b)) ni) dni *)
(* Goal: lt (nweight_Sequent nf_nil DNil (rev_app DNI_NIL ni1) (AVL_intro nf_list ai avl_ai)) (S n) *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply lt_ks_shift_nd with k; assumption.
(* Goal: lt (nweight_Sequent nf_nil DNil (rev_app DNI_NIL ni1) (AVL_intro nf_list ai avl_ai)) (S n) *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
simpl in |- *.
 rewrite
 (nweight_sequent_eqv nf_nil DNil ni1
    (rev_app dni (Undecorated (NImp a0 a1 b) :: ni))
    (AVL_intro nf_list ai avl_ai)).
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
assumption.
(* Goal: eqv_ni ni1 (rev_app dni (@cons nested_imp (Undecorated (NImp a0 a1 b)) ni)) *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply eqv_ni_trans with (rev_app dni (Decorated (NImp a0 a1 b) k :: ni)).
(* Goal: eqv_ni ni ni1 *)
(* Goal: lt (nweight_Sequent nf_nil (@cons (prod Int Int) (@pair Int Int i j) ds) ni (AVL_intro nf_list ai avl_ai)) (S n) *)
(* Goal: forall (ni2 : nested_imps) (_ : eqv_ni ni2 ni), nsearch_spec goal (@cons normal_form (NAtom j) nf_nil) ds ni2 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) (@cons form (Atom j) context) *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply le_eqv; assumption.
(* Goal: eqv_ni (rev_app dni (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni)) (rev_app dni (@cons nested_imp (Undecorated (NImp a0 a1 b)) ni)) *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply le_eqv.
(* Goal: le_ni (rev_app dni (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni)) (rev_app dni (@cons nested_imp (Undecorated (NImp a0 a1 b)) ni)) *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
 rewrite (rev_app_app dni (Decorated (NImp a0 a1 b) k :: ni)).
(* Goal: le_ni (@app nested_imp (rev_app dni NNil) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni)) (rev_app dni (@cons nested_imp (Undecorated (NImp a0 a1 b)) ni)) *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
 rewrite (rev_app_app dni (Undecorated (NImp a0 a1 b) :: ni)).
(* Goal: le_ni (@app nested_imp (rev_app dni NNil) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni)) (@app nested_imp (rev_app dni NNil) (@cons nested_imp (Undecorated (NImp a0 a1 b)) ni)) *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply le_ni_app_dn.
(* Goal: @eq nested_imps NNil NNil *)
(* Goal: lt (nweight_Sequent work DNil NNil AI_Nil) (S (nweight_Sequent work DNil NNil AI_Nil)) *)
(* Goal: REGULAR normal_form AI_Nil *)
(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
trivial.
(* Goal: le_ni (@app nested_imp (rev_app dni NNil) ni) (@app nested_imp (rev_app dni NNil) ni) *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply le_ni_refl.

(* Goal: forall (n0 : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 (@cons nested_imp (Decorated n0 k) l) dni) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni1 ni1) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context) (_ : lt (nweight_Sequent nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil DNil (rev_app dni (@cons nested_imp (Decorated n0 k) l)) (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
intros x k ni ih lt_nweight.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply shift_ni_dni; try assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply ih; try assumption.
(* Goal: Lt_Ks ni (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree x k) dni) (@cons nested_imp (Decorated x k) ni) dni *)
(* Goal: forall (d : disj) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj d l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply lt_ks_shift_dd.

(* ds=(cons (d0,d1) ds) *)
(* Goal: forall (d : unit) (_ : lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros d; case d; clear d.
(* Goal: forall (i i0 : Int) (l : list disj) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a : avl_tree unit) (avl_a : is_avl unit a) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a avl_a) goal) (_ : a_ai_disj (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent nf_nil (@cons disj (@pair Int Int i i0) l) ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal nf_nil (@cons disj (@pair Int Int i i0) l) ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
intros i j ds ni ai avl_ai a avl_a ai_reg a_goal_disj a_ai_disj lt_nweight.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply left_disj; try assumption.
(* Goal: forall (ni1 : nested_imps) (_ : le_ni ni1 NNil) (_ : deco_sound work DNil ni1 AI_Nil ANil) (_ : nsearch_spec_result_aux goal work DNil ni1 AI_Nil ANil context), nsearch_spec_result_aux goal work DNil NNil AI_Nil ANil context *)
(* Goal: lt (nweight_Sequent work DNil NNil AI_Nil) (S (nweight_Sequent work DNil NNil AI_Nil)) *)
(* Goal: REGULAR normal_form AI_Nil *)
(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
intros ni1 le1.
(* Goal: nsearch_spec goal (@app normal_form bs work) ds ni (AVL_intro nf_list ai' avl_ai') (AVL_intro unit a' avl_a') context *)
(* Goal: forall _ : forall d : nf_list, not (lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply ih_n; try assumption.
(* Goal: lt (nweight_Sequent (@cons normal_form (NAtom i) nf_nil) ds ni1 (AVL_intro nf_list ai avl_ai)) n *)
(* Goal: forall (ni2 : nested_imps) (_ : eqv_ni ni2 ni), nsearch_spec goal (@cons normal_form (NAtom j) nf_nil) ds ni2 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) (@cons form (Atom j) context) *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply nweight_sequent_left_disj_left with j ni.
(* Goal: eqv_ni ni ni1 *)
(* Goal: lt (nweight_Sequent nf_nil (@cons (prod Int Int) (@pair Int Int i j) ds) ni (AVL_intro nf_list ai avl_ai)) (S n) *)
(* Goal: forall (ni2 : nested_imps) (_ : eqv_ni ni2 ni), nsearch_spec goal (@cons normal_form (NAtom j) nf_nil) ds ni2 (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) (@cons form (Atom j) context) *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply le_eqv; assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
assumption.

(* Goal: forall (ni1 : nested_imps) (_ : le_ni ni1 NNil) (_ : deco_sound work DNil ni1 AI_Nil ANil) (_ : nsearch_spec_result_aux goal work DNil ni1 AI_Nil ANil context), nsearch_spec_result_aux goal work DNil NNil AI_Nil ANil context *)
(* Goal: lt (nweight_Sequent work DNil NNil AI_Nil) (S (nweight_Sequent work DNil NNil AI_Nil)) *)
(* Goal: REGULAR normal_form AI_Nil *)
(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
intros ni1 le1.
(* Goal: nsearch_spec goal (@app normal_form bs work) ds ni (AVL_intro nf_list ai' avl_ai') (AVL_intro unit a' avl_a') context *)
(* Goal: forall _ : forall d : nf_list, not (lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply ih_n; try assumption.
(* Goal: lt (nweight_Sequent (@cons normal_form (NAtom j) nf_nil) ds ni1 (AVL_intro nf_list ai avl_ai)) n *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
apply nweight_sequent_left_disj_right with i ni.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply eqv_sym; assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
assumption.

(* work=(cons .. *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : forall (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent l ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal l ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context) (ds : disjs) (ni : nested_imps) (ai : avl_tree nf_list) (avl_ai : is_avl nf_list ai) (a0 : avl_tree unit) (avl_a : is_avl unit a0) (_ : REGULAR normal_form (AVL_intro nf_list ai avl_ai)) (_ : a_goal_disj (AVL_intro unit a0 avl_a) goal) (_ : a_ai_disj (AVL_intro unit a0 avl_a) (AVL_intro nf_list ai avl_ai)) (_ : lt (nweight_Sequent (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form a l) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a0 avl_a) context *)
intros c work ih_work ds ni ai avl_ai a avl_a ai_reg a_goal_disj a_ai_disj.
(* Goal: forall _ : lt (nweight_Sequent (@cons normal_form c work) ds ni (AVL_intro nf_list ai avl_ai)) (S n), nsearch_spec goal (@cons normal_form c work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
case c; clear c.

(* a=NFalsum*)
(* Goal: forall _ : lt (nweight_Sequent (@cons normal_form NFalsum work) ds ni (AVL_intro nf_list ai avl_ai)) (S n), nsearch_spec goal (@cons normal_form NFalsum work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (_ : lt (nweight_Sequent (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros lt_nweight.
(* Goal: forall _ : Equal goal i, nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : not (Equal goal i), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
clear ih_work ih_n.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply nefq; assumption.

(* a=(NAtom i)  *)
(* Goal: forall (i : Int) (_ : lt (nweight_Sequent (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros i lt_nweight.
(* Goal: nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
elim (equal_dec goal i).
(* Goal: forall _ : Equal goal i, nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : not (Equal goal i), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
clear ih_work ih_n.
(* Goal: forall _ : Equal goal i, nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : not (Equal goal i), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros equal_goal.
(* Goal: nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : not (Equal goal i), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply nax; try assumption.
(* Goal: in_ngamma (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) (NAtom goal) *)
(* Goal: forall _ : not (Equal goal i), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
 rewrite (equal_eq goal i equal_goal).
(* Goal: in_ngamma (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) (NAtom i) *)
(* Goal: forall _ : not (Equal goal i), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply in_ngamma_cons_work_head.

(* Goal: forall _ : not (Equal goal i), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros not_equal_goal.
(* Goal: nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
elim (insert_avl unit i (fun x : unit => tt) tt a avl_a).
(* Goal: forall (t : avl_tree unit) (_ : lookup_dec_spec unit i a) (_ : is_avl unit t) (_ : lin_ins_spec unit i (fun _ : unit => tt) tt a t) (_ : equiv_ins unit i (fun _ : unit => tt) tt a t) (_ : sumbool (@eq nat (height_avl unit t) (height_avl unit a)) (@eq nat (height_avl unit t) (S (height_avl unit a)))), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros a' lookup_dec_a avl_a' lin_ins equiv_ins height_dec; clear height_dec.
(* Goal: nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
elim lookup_dec_a; clear lookup_dec_a lin_ins.
(* Goal: forall (d : unit) (_ : lookup unit i a d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
clear ih_n.
(* Goal: forall (d : unit) (_ : lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros d; case d; clear d.
(* Goal: forall _ : lookup unit i a tt, nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros lookup.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply contradiction_atoms; try assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply ih_work; clear ih_work; assumption.

(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros not_lookup.
(* Goal: nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
elim (delete_avl nf_list i ai avl_ai).
intros ai' lookup_dec_ai' avl_ai' lin_del equiv_del height_dec;
 clear height_dec.
(* Goal: nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
elim lookup_dec_ai'; clear lookup_dec_ai'.
(* Goal: forall (d : nf_list) (_ : lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : forall d : nf_list, not (lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros bs lookup_bs; clear ih_work.
apply
 left_p_imp_ai
  with bs (AVL_intro nf_list ai' avl_ai') (AVL_intro unit a' avl_a');
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
 try assumption.
(* Goal: nsearch_spec goal (@app normal_form bs work) ds ni (AVL_intro nf_list ai' avl_ai') (AVL_intro unit a' avl_a') context *)
(* Goal: forall _ : forall d : nf_list, not (lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply ih_n; try assumption.
apply
 lt_le_trans with (nweight_Sequent work ds ni (AVL_intro nf_list ai avl_ai)).
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply nweight_shift_ai_work with i; try assumption.
(* Goal: LIN_DEL nf_list i bs (AVL_intro nf_list ai avl_ai) (AVL_intro nf_list ai' avl_ai') *)
(* Goal: le (nweight_Sequent work ds ni (AVL_intro nf_list ai avl_ai)) n *)
(* Goal: REGULAR normal_form (AVL_intro nf_list ai' avl_ai') *)
(* Goal: Disjunct.a_ai_disj (AVL_intro unit a' avl_a') (AVL_intro nf_list ai' avl_ai') *)
(* Goal: Disjunct.a_goal_disj (AVL_intro unit a' avl_a') goal *)
(* Goal: forall _ : forall d : nf_list, not (lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
unfold LIN_DEL in |- *.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply lin_del; assumption.
(* Goal: le (nweight_Sequent work ds ni (AVL_intro nf_list ai avl_ai)) n *)
(* Goal: REGULAR normal_form (AVL_intro nf_list ai' avl_ai') *)
(* Goal: Disjunct.a_ai_disj (AVL_intro unit a' avl_a') (AVL_intro nf_list ai' avl_ai') *)
(* Goal: Disjunct.a_goal_disj (AVL_intro unit a' avl_a') goal *)
(* Goal: forall _ : forall d : nf_list, not (lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
inversion_clear lt_nweight.
(* Goal: le (nweight_Sequent work ds ni (AVL_intro nf_list ai avl_ai)) (nweight_Sequent (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai)) *)
(* Goal: le (nweight_Sequent work ds ni (AVL_intro nf_list ai avl_ai)) n *)
(* Goal: REGULAR normal_form (AVL_intro nf_list ai' avl_ai') *)
(* Goal: Disjunct.a_ai_disj (AVL_intro unit a' avl_a') (AVL_intro nf_list ai' avl_ai') *)
(* Goal: Disjunct.a_goal_disj (AVL_intro unit a' avl_a') goal *)
(* Goal: forall _ : forall d : nf_list, not (lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply le_n.
(* Goal: le (nweight_Sequent work ds ni (AVL_intro nf_list ai avl_ai)) n *)
(* Goal: REGULAR normal_form (AVL_intro nf_list ai' avl_ai') *)
(* Goal: Disjunct.a_ai_disj (AVL_intro unit a' avl_a') (AVL_intro nf_list ai' avl_ai') *)
(* Goal: Disjunct.a_goal_disj (AVL_intro unit a' avl_a') goal *)
(* Goal: forall _ : forall d : nf_list, not (lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply le_Sn_le.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
assumption.

(* side premisses: Apply ih_n.  *)
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply regular_EQUIV_DEL with i (AVL_intro nf_list ai avl_ai); assumption.
apply
 disjs_delete_ai
  with i (AVL_intro unit a avl_a) (AVL_intro nf_list ai avl_ai); 
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
 assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply goal_disj_insert_a with i (AVL_intro unit a avl_a); assumption.

(* Goal: forall _ : forall d : nf_list, not (lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (NAtom i) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros not_lookup_bs.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply rule_shift_work_a with (AVL_intro unit a' avl_a'); try assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply ih_work; clear ih_work; try assumption.
(* side premisses: Apply ih_work.  *)
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply goal_disj_insert_a with i (AVL_intro unit a avl_a); assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply disjs_insert_a with i (AVL_intro unit a avl_a); assumption.

(* a=(OrF (Atom i) (Atom j)) *)
(* Goal: forall (i i0 : Int) (_ : lt (nweight_Sequent (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NDisj i i0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros i j lt_nweight.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply rule_shift_work_ds; try assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply ih_work; clear ih_work; try assumption.
 rewrite <-
 (nweight_shift_work_ds i j work ds ni (AVL_intro nf_list ai avl_ai))
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
 ; assumption.

(* a=(AImp i b) *)
(* Goal: forall (i : Int) (n0 : normal_form) (_ : lt (nweight_Sequent (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (AImp i n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros i b lt_nweight.
(* Goal: nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
elim (lookup_dec unit i a avl_a).
(* Goal: forall (d : unit) (_ : lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros d; case d; clear d.
(* Goal: forall _ : lookup unit i a tt, nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros lookup_i.
(* Goal: nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
clear ih_work.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply left_p_imp_work; try assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply ih_n; clear ih_n; try assumption.
(* Goal: lt (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai)) n *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply lt_S_n.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
assumption.

(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros not_lookup_i.
(* Goal: nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
elim (insert_avl nf_list i (cons b) nf_nil ai avl_ai).
(* Goal: forall (t : avl_tree nf_list) (_ : lookup_dec_spec nf_list i ai) (_ : is_avl nf_list t) (_ : lin_ins_spec nf_list i (@cons normal_form b) nf_nil ai t) (_ : equiv_ins nf_list i (@cons normal_form b) nf_nil ai t) (_ : sumbool (@eq nat (height_avl nf_list t) (height_avl nf_list ai)) (@eq nat (height_avl nf_list t) (S (height_avl nf_list ai)))), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros ai' lookup_dec avl_ai' lin_ins equiv_ins height_dec; clear height_dec.
(* Goal: nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
elim lookup_dec; clear lookup_dec.
(* Goal: forall (d : nf_list) (_ : lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall _ : forall d : nf_list, not (lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros bs lookup_bs.
apply rule_shift_work_ai_old with bs (AVL_intro nf_list ai' avl_ai');
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
 try assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply ih_work; clear ih_work; try assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply regular_EQUIV_INS with i b (AVL_intro nf_list ai avl_ai); assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply disjs_insert_ai with i b (AVL_intro nf_list ai avl_ai); assumption.
 rewrite <-
 (nweight_shift_work_ai i b work ds ni (AVL_intro nf_list ai avl_ai)
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
    (AVL_intro nf_list ai' avl_ai')); assumption.
(* Goal: forall _ : forall d : nf_list, not (lookup nf_list i ai d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros notlookup_bs.
apply rule_shift_work_ai_new with (AVL_intro nf_list ai' avl_ai');
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
 try assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply ih_work; clear ih_work; try assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply regular_EQUIV_INS with i b (AVL_intro nf_list ai avl_ai); assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply disjs_insert_ai with i b (AVL_intro nf_list ai avl_ai); assumption.
 rewrite <-
 (nweight_shift_work_ai i b work ds ni (AVL_intro nf_list ai avl_ai)
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
    (AVL_intro nf_list ai' avl_ai')); assumption.


(* a=(NImp x) *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros x lt_nweight.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply rule_shift_work_ni0; try assumption.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply ih_work; clear ih_work; try assumption.
 rewrite <-
 (nweight_shift_work_ni0 x work ds ni (AVL_intro nf_list ai avl_ai))
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
 ; assumption.
Qed.




Theorem nsearch :
 forall (goal : Int) (work : nf_list) (context : flist),
 (forall (n : nat) (a : normal_form),
  my_nth normal_form n work a -> Derivable context (nf2form a)) ->
 (forall (a : form) (k : kripke_tree),
  Is_Monotone_kripke_tree k ->
  (forall b : normal_form, In b work -> forces_t k (nf2form b)) ->
  In a context -> forces_t k a) ->
 nsearch_spec_result_aux goal work DNil NNil AI_Nil ANil context.
(* Goal: forall (goal : Int) (work : nf_list) (context : flist) (_ : forall (n : nat) (a : normal_form) (_ : my_nth normal_form n work a), Derivable context (nf2form a)) (_ : forall (a : form) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (_ : forall (b : normal_form) (_ : @In normal_form b work), forces_t k (nf2form b)) (_ : @In form a context), forces_t k a), nsearch_spec_result_aux goal work DNil NNil AI_Nil ANil context *)
intros goal work context sound minimal.
elim
 (nsearch_aux (S (nweight_Sequent work DNil NNil AI_Nil)) goal work DNil NNil
    AI_Nil ANil context).
(* Goal: forall (ni1 : nested_imps) (_ : le_ni ni1 NNil) (_ : deco_sound work DNil ni1 AI_Nil ANil) (_ : nsearch_spec_result_aux goal work DNil ni1 AI_Nil ANil context), nsearch_spec_result_aux goal work DNil NNil AI_Nil ANil context *)
(* Goal: lt (nweight_Sequent work DNil NNil AI_Nil) (S (nweight_Sequent work DNil NNil AI_Nil)) *)
(* Goal: REGULAR normal_form AI_Nil *)
(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
intros ni1 le1.
(* Goal: forall (_ : deco_sound work DNil ni1 AI_Nil ANil) (_ : nsearch_spec_result_aux goal work DNil ni1 AI_Nil ANil context), nsearch_spec_result_aux goal work DNil NNil AI_Nil ANil context *)
(* Goal: lt (nweight_Sequent work DNil NNil AI_Nil) (S (nweight_Sequent work DNil NNil AI_Nil)) *)
(* Goal: REGULAR normal_form AI_Nil *)
(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
cut (ni1 = NNil).
(* Goal: forall (_ : @eq nested_imps ni1 NNil) (_ : deco_sound work DNil ni1 AI_Nil ANil) (_ : nsearch_spec_result_aux goal work DNil ni1 AI_Nil ANil context), nsearch_spec_result_aux goal work DNil NNil AI_Nil ANil context *)
(* Goal: @eq nested_imps ni1 NNil *)
(* Goal: lt (nweight_Sequent work DNil NNil AI_Nil) (S (nweight_Sequent work DNil NNil AI_Nil)) *)
(* Goal: REGULAR normal_form AI_Nil *)
(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
intros claim.
(* Goal: forall (_ : deco_sound work DNil ni1 AI_Nil ANil) (_ : nsearch_spec_result_aux goal work DNil ni1 AI_Nil ANil context), nsearch_spec_result_aux goal work DNil NNil AI_Nil ANil context *)
(* Goal: @eq nested_imps ni1 NNil *)
(* Goal: lt (nweight_Sequent work DNil NNil AI_Nil) (S (nweight_Sequent work DNil NNil AI_Nil)) *)
(* Goal: REGULAR normal_form AI_Nil *)
(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
 rewrite claim.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
intros; assumption.
(* Goal: @eq nested_imps ni1 NNil *)
(* Goal: lt (nweight_Sequent work DNil NNil AI_Nil) (S (nweight_Sequent work DNil NNil AI_Nil)) *)
(* Goal: REGULAR normal_form AI_Nil *)
(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
inversion_clear le1.
(* Goal: @eq nested_imps NNil NNil *)
(* Goal: lt (nweight_Sequent work DNil NNil AI_Nil) (S (nweight_Sequent work DNil NNil AI_Nil)) *)
(* Goal: REGULAR normal_form AI_Nil *)
(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
trivial.
(* Goal: lt (nweight_Sequent work DNil NNil AI_Nil) (S (nweight_Sequent work DNil NNil AI_Nil)) *)
(* Goal: REGULAR normal_form AI_Nil *)
(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
apply lt_n_Sn.

(* Goal: REGULAR normal_form AI_Nil *)
(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
unfold AI_Nil in |- *.
(* Goal: REGULAR normal_form (AVL_NIL nf_list) *)
(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
unfold nf_list in |- *.
(* Goal: REGULAR normal_form (AVL_NIL (list normal_form)) *)
(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
apply regular_AVL_NIL.

(* Goal: a_ai_disj ANil AI_Nil *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
unfold a_ai_disj in |- *.
(* Goal: forall (i : Int) (_ : LOOKUP unit i ANil tt) (bs : nf_list) (_ : LOOKUP nf_list i AI_Nil bs), False *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
intros i lookup_i bs lookup_bs.
(* Goal: False *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
inversion_clear lookup_i.

(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
unfold a_goal_disj in |- *.
(* Goal: forall _ : LOOKUP unit goal ANil tt, False *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
intros lookup_goal.
(* Goal: False *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
inversion_clear lookup_goal.

(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
unfold deco_sound in |- *.
(* Goal: forall (k : kripke_tree) (i0 i1 : Int) (b : normal_form) (_ : @In nested_imp (Decorated (NImp i0 i1 b) k) NNil), k_deco_sound k i0 i1 work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
intros k i0 i1 b in_k.
(* Goal: k_deco_sound k i0 i1 work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
inversion_clear in_k.

(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
unfold nsound in |- *.
(* Goal: forall (c : normal_form) (_ : in_ngamma work DNil NNil AI_Nil ANil c), Derivable context (nf2form c) *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
intros a in_ngamma.
(* Goal: Derivable context (nf2form a) *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
elim in_ngamma; clear in_ngamma a.

(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), Derivable context (nf2form c) *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n DNil (@pair Int Int i j)), Derivable context (nf2form (NDisj i j)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps NNil) x), Derivable context (nf2form (NImp_NF x)) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i AI_Nil bs) (_ : my_nth normal_form n bs b), Derivable context (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i ANil tt), Derivable context (nf2form (NAtom i)) *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
intros n a nth.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply sound with n; assumption.

(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n DNil (@pair Int Int i j)), Derivable context (nf2form (NDisj i j)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps NNil) x), Derivable context (nf2form (NImp_NF x)) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i AI_Nil bs) (_ : my_nth normal_form n bs b), Derivable context (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i ANil tt), Derivable context (nf2form (NAtom i)) *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
intros n i j nth; elimtype False; inversion_clear nth.
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps NNil) x), Derivable context (nf2form (NImp_NF x)) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i AI_Nil bs) (_ : my_nth normal_form n bs b), Derivable context (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i ANil tt), Derivable context (nf2form (NAtom i)) *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
intros n x nth; elimtype False; inversion_clear nth.
(* Goal: False *)
(* Goal: a_goal_disj ANil goal *)
(* Goal: deco_sound work DNil NNil AI_Nil ANil *)
(* Goal: nsound work DNil NNil AI_Nil ANil context *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
intros i b n bs lookup_i nth; elimtype False; inversion_clear lookup_i.
(* Goal: forall (i : Int) (_ : LOOKUP unit i ANil tt), Derivable context (nf2form (NAtom i)) *)
(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
intros i lookup; elimtype False; inversion_clear lookup.

(* Goal: nminimal work DNil NNil AI_Nil ANil context *)
unfold nminimal in |- *.
(* Goal: forall (c : form) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (_ : forces_ngamma work DNil NNil AI_Nil ANil k) (_ : @In form c context), forces_t k c *)
intros a k k_is_mon k_forces_gamma in_a.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply minimal; try assumption.
(* Goal: forall (b : normal_form) (_ : @In normal_form b work), forces_t k (nf2form b) *)
intros b in_b.
(* Goal: forces_t k (nf2form b) *)
elim (in_nth normal_form b work in_b).
(* Goal: forall (x : nat) (_ : my_nth normal_form x work b), forces_t k (nf2form b) *)
intros n nth.
(* Goal: forces_t k (nf2form b) *)
apply k_forces_gamma.
(* Goal: lt (S (nweight_Sequent (@cons normal_form b work) ds ni (AVL_intro nf_list ai avl_ai))) (S n) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i a d), nsearch_spec goal (@cons normal_form (AImp i b) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
(* Goal: forall (n0 : nimp) (_ : lt (nweight_Sequent (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai)) (S n)), nsearch_spec goal (@cons normal_form (NImp_NF n0) work) ds ni (AVL_intro nf_list ai avl_ai) (AVL_intro unit a avl_a) context *)
apply In_Work with n; assumption.
Qed.