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

(*******************************************************************)
(* The left hand side Gamma of a sequent consists of               *)
(*     work : a list of (arbitray) normalforms                     *)
(*            (to be inserted in the following structures)         *)
(*     ds: a list of disjunctions                                  *)
(*     ni: a list of decorated and undecorated nested implications *)
(*     ai: an AVL tree of atomic implications                      *)
(*     a: an AVL tree of atoms                                     *)
(*******************************************************************)

Require Export Kripke_Trees.
Require Export Normal_Forms.



(************************************************************)
(* disjunctions are stored as pairs of Int's                *)

Definition disj := (Int * Int)%type.
Definition disjs := list disj.
Definition DNil := nil (A:=disj).

Definition disj2form (x : disj) :=
  match x with
  | (i, j) => OrF (Atom i) (Atom j)
  end.

Definition disj2nform (x : disj) := match x with
                                    | (i, j) => NDisj i j
                                    end.

Definition disjs2forms (ds : disjs) := map disj2form ds.
Definition disjs2nforms (ds : disjs) := map disj2nform ds.


(*****************************************************************)
(* Nested implications are stored either as a nimp or as a       *)
(* nimp and a counter-model                                      *)

Inductive nested_imp : Set :=
  | Undecorated : nimp -> nested_imp
  | Decorated : nimp -> kripke_tree -> nested_imp.

Definition nested_imp2nimp (ni : nested_imp) :=
  match ni with
  | Undecorated ni => ni
  | Decorated ni _ => ni
  end.


Definition nested_imp2form (x : nested_imp) := nimp2form (nested_imp2nimp x).
Definition nested_imp2nform (x : nested_imp) := NImp_NF (nested_imp2nimp x).

Definition nested_imps := list nested_imp.
Definition NNil := nil (A:=nested_imp).

Definition nested_imps2forms (ni : nested_imps) := map nested_imp2form ni.
Definition nested_imps2nforms (ni : nested_imps) := map nested_imp2nform ni.
Definition nested_imps2nimps (ni : nested_imps) := map nested_imp2nimp ni.


Lemma nested_imps2nimps_app :
 forall ni1 ni2 : nested_imps,
 nested_imps2nimps (ni1 ++ ni2) =
 nested_imps2nimps ni1 ++ nested_imps2nimps ni2.
(* Goal: forall ni1 ni2 : nested_imps, @eq (list nimp) (nested_imps2nimps (@app nested_imp ni1 ni2)) (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) *)
intros ni1 ni2.
(* Goal: @eq (list nimp) (nested_imps2nimps (@app nested_imp ni1 ni2)) (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) *)
elim ni1; clear ni1.
(* Goal: @eq nat (@length nested_imp (@nil nested_imp)) (@length nimp (nested_imps2nimps (@nil nested_imp))) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : @eq nat (@length nested_imp l) (@length nimp (nested_imps2nimps l))), @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nimp (nested_imps2nimps (@cons nested_imp a l))) *)
simpl in |- *; trivial.
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : @eq (list nimp) (nested_imps2nimps (@app nested_imp l ni2)) (@app nimp (nested_imps2nimps l) (nested_imps2nimps ni2))), @eq (list nimp) (nested_imps2nimps (@app nested_imp (@cons nested_imp a l) ni2)) (@app nimp (nested_imps2nimps (@cons nested_imp a l)) (nested_imps2nimps ni2)) *)
intros x ni1 ih.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: @eq nat (S (@length nested_imp ni)) (S (@length nimp (nested_imps2nimps ni))) *)
 rewrite ih; trivial.
Qed.


Lemma nested_imps2nimps_length :
 forall ni : nested_imps, length ni = length (nested_imps2nimps ni).
(* Goal: forall ni : nested_imps, @eq nat (@length nested_imp ni) (@length nimp (nested_imps2nimps ni)) *)
intros ni; elim ni; clear ni.
(* Goal: @eq nat (@length nested_imp (@nil nested_imp)) (@length nimp (nested_imps2nimps (@nil nested_imp))) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : @eq nat (@length nested_imp l) (@length nimp (nested_imps2nimps l))), @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nimp (nested_imps2nimps (@cons nested_imp a l))) *)
simpl in |- *; trivial.
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : @eq nat (@length nested_imp l) (@length nimp (nested_imps2nimps l))), @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nimp (nested_imps2nimps (@cons nested_imp a l))) *)
intros x ni ih.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: @eq nat (S (@length nested_imp ni)) (S (@length nimp (nested_imps2nimps ni))) *)
 rewrite ih; trivial.
Qed.

(************************************************************************)
(* Atomic implactions are stored in AVL Trees ai over lists of normal   *)
(* clauses.                                                             *)
(* For the node with the key field=i and with the data field=bs,        *)
(* we define that, for each b in bs, (Imp (Atom i) b) is in ai.         *)

Definition atomic_imps := AVL nf_list.
Definition AI_Nil := AVL_NIL nf_list.


(************************************************************************)
(* Atoms are stored in AVL Trees ai over unit.                          *)
(* For the node with the key field=i,                                   *)
(* we define that (Atom i) is in ai.                                    *)
(* (Definition in Kripke_Trees.v                                        *)


(************************************************************************)
(* The formulae on the left-hand side of the sequent are given by:      *)

Inductive in_ngamma (work : nf_list) (ds : disjs) (ni : nested_imps)
(ai : atomic_imps) (a : atoms) : normal_form -> Set :=
  | In_Work :
      forall (n : nat) (c : normal_form),
      my_nth normal_form n work c -> in_ngamma work ds ni ai a c
  | In_Disjs :
      forall (n : nat) (i j : Int),
      my_nth disj n ds (i, j) -> in_ngamma work ds ni ai a (NDisj i j)
  | In_Nested_Imps :
      forall (n : nat) (x : nimp),
      my_nth nimp n (nested_imps2nimps ni) x ->
      in_ngamma work ds ni ai a (NImp_NF x)
  | In_Atomic_Imps :
      forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list),
      LOOKUP nf_list i ai bs ->
      my_nth normal_form n bs b -> in_ngamma work ds ni ai a (AImp i b)
  | In_Atoms :
      forall i : Int,
      LOOKUP unit i a tt -> in_ngamma work ds ni ai a (NAtom i).


(********************************************************************)


Lemma in_ngamma_cons_work_tail :
 forall (c0 : normal_form) (work : nf_list) (ds : disjs) 
   (ni : nested_imps) (ai : atomic_imps) (a : atoms) 
   (c : normal_form),
 in_ngamma work ds ni ai a c -> in_ngamma (c0 :: work) ds ni ai a c.
(* Goal: forall (c0 : normal_form) (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma (@cons normal_form c0 work) ds ni ai a c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c c0) *)
intros c0 work ds ni ai a c in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), in_ngamma (@cons normal_form c0 work) ds ni ai a c *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma (@cons normal_form c0 work) ds ni ai a (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma (@cons normal_form c0 work) ds ni ai a (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma (@cons normal_form c0 work) ds ni ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma (@cons normal_form c0 work) ds ni ai a (NAtom i) *)
intros n a0 nth; apply In_Work with (S n); apply My_NthS; assumption.
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni' ai a (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni' ai a (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni' ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni' ai a (NAtom i) *)
intros n i j nth; apply In_Disjs with n; assumption.
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai' a (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai' a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros n x nth; apply In_Nested_Imps with n; assumption.
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
intros i b n bs lookup nth; apply In_Atomic_Imps with n bs; assumption.
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
intros i lookup; apply In_Atoms; assumption.
Qed.

Lemma in_ngamma_cons_work_head :
 forall (c : normal_form) (work : nf_list) (ds : disjs) 
   (ni : nested_imps) (ai : atomic_imps) (a : atoms),
 in_ngamma (c :: work) ds ni ai a c.
(* Goal: forall (c : normal_form) (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms), in_ngamma (@cons normal_form c work) ds ni ai a c *)
intros c work ds ni ai a.
(* Goal: in_ngamma (@cons normal_form c work) ds ni ai a c *)
apply In_Work with 0.
(* Goal: my_nth normal_form O (@cons normal_form b bs) b *)
apply My_NthO.
Qed.


Lemma in_ngamma_work_app1 :
 forall (bs work : nf_list) (ds : disjs) (ni : nested_imps)
   (ai : atomic_imps) (a : atoms) (c : normal_form),
 in_ngamma work ds ni ai a c -> in_ngamma (bs ++ work) ds ni ai a c.
(* Goal: forall (bs work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma (@app normal_form bs work) ds ni ai a c), sum (in_ngamma work ds ni ai a c) (@sig nat (fun n : nat => my_nth normal_form n bs c)) *)
intros bs work ds ni ai a c in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n (@app normal_form bs work) c), sum (in_ngamma work ds ni ai a c) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs c)) *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), sum (in_ngamma work ds ni ai a (NDisj i j)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (NDisj i j))) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sum (in_ngamma work ds ni ai a (NImp_NF x)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (NImp_NF x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs0 : nf_list) (_ : LOOKUP nf_list i ai bs0) (_ : my_nth normal_form n bs0 b), sum (in_ngamma work ds ni ai a (AImp i b)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (AImp i b))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sum (in_ngamma work ds ni ai a (NAtom i)) (@sig nat (fun n : nat => my_nth normal_form n bs (NAtom i))) *)
intros n c0 nth. 
(* Goal: in_ngamma (@app normal_form bs work) ds ni ai a c0 *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma (@app normal_form bs work) ds ni ai a (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma (@app normal_form bs work) ds ni ai a (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs0 : nf_list) (_ : LOOKUP nf_list i ai bs0) (_ : my_nth normal_form n bs0 b), in_ngamma (@app normal_form bs work) ds ni ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma (@app normal_form bs work) ds ni ai a (NAtom i) *)
apply In_Work with (length bs + n); apply nth_app1; assumption.
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni' ai a (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni' ai a (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni' ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni' ai a (NAtom i) *)
intros n i j nth; apply In_Disjs with n; assumption.
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai' a (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai' a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros n x nth; apply In_Nested_Imps with n; assumption.
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs0 : nf_list) (_ : LOOKUP nf_list i ai bs0) (_ : my_nth normal_form n bs0 b), in_ngamma (@app normal_form bs work) ds ni ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma (@app normal_form bs work) ds ni ai a (NAtom i) *)
intros i b n bs' lookup nth; apply In_Atomic_Imps with n bs'; assumption.
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
intros i lookup; apply In_Atoms; assumption.
Qed.







Lemma in_ngamma_work_app_rev :
 forall (bs work : nf_list) (ds : disjs) (ni : nested_imps)
   (ai : atomic_imps) (a : atoms) (c : normal_form),
 in_ngamma (bs ++ work) ds ni ai a c ->
 in_ngamma work ds ni ai a c + {n : nat | my_nth normal_form n bs c}.
(* Goal: forall (bs work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma (@app normal_form bs work) ds ni ai a c), sum (in_ngamma work ds ni ai a c) (@sig nat (fun n : nat => my_nth normal_form n bs c)) *)
intros bs work ds ni ai a c in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n (@app normal_form bs work) c), sum (in_ngamma work ds ni ai a c) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs c)) *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), sum (in_ngamma work ds ni ai a (NDisj i j)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (NDisj i j))) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sum (in_ngamma work ds ni ai a (NImp_NF x)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (NImp_NF x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs0 : nf_list) (_ : LOOKUP nf_list i ai bs0) (_ : my_nth normal_form n bs0 b), sum (in_ngamma work ds ni ai a (AImp i b)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (AImp i b))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sum (in_ngamma work ds ni ai a (NAtom i)) (@sig nat (fun n : nat => my_nth normal_form n bs (NAtom i))) *)
intros n c0 nth. 
(* Goal: sum (in_ngamma work ds ni ai a c0) (@sig nat (fun n : nat => my_nth normal_form n bs c0)) *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), sum (in_ngamma work ds ni ai a (NDisj i j)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (NDisj i j))) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sum (in_ngamma work ds ni ai a (NImp_NF x)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (NImp_NF x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs0 : nf_list) (_ : LOOKUP nf_list i ai bs0) (_ : my_nth normal_form n bs0 b), sum (in_ngamma work ds ni ai a (AImp i b)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (AImp i b))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sum (in_ngamma work ds ni ai a (NAtom i)) (@sig nat (fun n : nat => my_nth normal_form n bs (NAtom i))) *)
elim (inv_nth_app normal_form n bs work c0 nth); clear nth.
(* Goal: forall _ : my_nth normal_form n bs c0, sum (in_ngamma work ds ni ai a c0) (@sig nat (fun n : nat => my_nth normal_form n bs c0)) *)
(* Goal: forall (n' : nat) (_ : my_nth normal_form n' work c0), sum (in_ngamma work ds ni ai a c0) (@sig nat (fun n : nat => my_nth normal_form n bs c0)) *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), sum (in_ngamma work ds ni ai a (NDisj i j)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (NDisj i j))) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sum (in_ngamma work ds ni ai a (NImp_NF x)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (NImp_NF x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs0 : nf_list) (_ : LOOKUP nf_list i ai bs0) (_ : my_nth normal_form n bs0 b), sum (in_ngamma work ds ni ai a (AImp i b)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (AImp i b))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sum (in_ngamma work ds ni ai a (NAtom i)) (@sig nat (fun n : nat => my_nth normal_form n bs (NAtom i))) *)
intros nth0; right; exists n; assumption.
(* Goal: forall (n' : nat) (_ : my_nth normal_form n' work c0), sum (in_ngamma work ds ni ai a c0) (@sig nat (fun n : nat => my_nth normal_form n bs c0)) *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), sum (in_ngamma work ds ni ai a (NDisj i j)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (NDisj i j))) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sum (in_ngamma work ds ni ai a (NImp_NF x)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (NImp_NF x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs0 : nf_list) (_ : LOOKUP nf_list i ai bs0) (_ : my_nth normal_form n bs0 b), sum (in_ngamma work ds ni ai a (AImp i b)) (@sig nat (fun n0 : nat => my_nth normal_form n0 bs (AImp i b))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sum (in_ngamma work ds ni ai a (NAtom i)) (@sig nat (fun n : nat => my_nth normal_form n bs (NAtom i))) *)
intros n' nth1; left; apply In_Work with n'; assumption.
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NDisj i j)) (@eq normal_form (NDisj i j) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (n : nat) (x0 : nimp) (_ : my_nth nimp n (nested_imps2nimps (@app nested_imp ni1 (@cons nested_imp x ni2))) x0), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros n i j nth; left; apply In_Disjs with n; assumption.
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) (AImp i b)) *)
(* Goal: forall (i0 : Int) (b0 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b0), sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros n x nth; left; apply In_Nested_Imps with n; assumption.
intros i b n bs' lookup nth; left; apply In_Atomic_Imps with n bs';
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
 assumption.
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros i lookup; left; apply In_Atoms; assumption.
Qed.




Lemma in_ngamma_cons_work_rev :
 forall (c0 : normal_form) (work : nf_list) (ds : disjs) 
   (ni : nested_imps) (ai : atomic_imps) (a : atoms) 
   (c : normal_form),
 in_ngamma (c0 :: work) ds ni ai a c ->
 in_ngamma work ds ni ai a c + {c = c0}.
(* Goal: forall (c0 : normal_form) (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma (@cons normal_form c0 work) ds ni ai a c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c c0) *)
intros c0 work ds ni ai a c in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (x0 : nimp) (_ : my_nth nimp n (nested_imps2nimps (@cons nested_imp x ni)) x0), sumor (in_ngamma work ds ni ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds ni ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros n; case n; clear n.
(* Goal: forall (c : normal_form) (_ : my_nth normal_form O (@cons normal_form c0 work) c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c c0) *)
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form (S n) (@cons normal_form c0 work) c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c c0) *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), sumor (in_ngamma work ds ni ai a (NDisj i j)) (@eq normal_form (NDisj i j) c0) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) c0) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i b)) (@eq normal_form (AImp i b) c0) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds ni ai a (NAtom i)) (@eq normal_form (NAtom i) c0) *)
intros a0 nth; right; inversion_clear nth; trivial.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form (S n) (@cons normal_form c0 work) c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c c0) *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), sumor (in_ngamma work ds ni ai a (NDisj i j)) (@eq normal_form (NDisj i j) c0) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) c0) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i b)) (@eq normal_form (AImp i b) c0) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds ni ai a (NAtom i)) (@eq normal_form (NAtom i) c0) *)
intros n c1 nth; left; apply In_Work with n; inversion_clear nth; assumption.
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NDisj i j)) (@eq normal_form (NDisj i j) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (n : nat) (x0 : nimp) (_ : my_nth nimp n (nested_imps2nimps (@app nested_imp ni1 (@cons nested_imp x ni2))) x0), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros n i j nth; left; apply In_Disjs with n; assumption.
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) (AImp i b)) *)
(* Goal: forall (i0 : Int) (b0 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b0), sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros n x nth; left; apply In_Nested_Imps with n; assumption.
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros i b n bs lookup nth; left; apply In_Atomic_Imps with n bs; assumption.
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros i lookup; left; apply In_Atoms; assumption.
Qed.



Lemma in_ngamma_cons_ds_tail :
 forall (work : nf_list) (i j : Int) (ds : disjs) (ni : nested_imps)
   (ai : atomic_imps) (a : atoms) (c : normal_form),
 in_ngamma work ds ni ai a c -> in_ngamma work ((i, j) :: ds) ni ai a c.
(* Goal: forall (work : nf_list) (i j : Int) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma work (@cons (prod Int Int) (@pair Int Int i j) ds) ni ai a c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NDisj i j)) *)
intros work i j ds ni ai a c in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), in_ngamma work ds ni ai a' c *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni ai a' (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai a' (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai a' (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai a' (NAtom i) *)
intros n c0 nth; apply In_Work with n; assumption.
(* Goal: forall (n : nat) (i0 j0 : Int) (_ : my_nth disj n ds (@pair Int Int i0 j0)), in_ngamma work (@cons (prod Int Int) (@pair Int Int i j) ds) ni ai a (NDisj i0 j0) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work (@cons (prod Int Int) (@pair Int Int i j) ds) ni ai a (NImp_NF x) *)
(* Goal: forall (i0 : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai bs) (_ : my_nth normal_form n bs b), in_ngamma work (@cons (prod Int Int) (@pair Int Int i j) ds) ni ai a (AImp i0 b) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), in_ngamma work (@cons (prod Int Int) (@pair Int Int i j) ds) ni ai a (NAtom i0) *)
intros n i' j' nth; apply In_Disjs with (S n); apply My_NthS; assumption.
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai' a (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai' a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros n x nth; apply In_Nested_Imps with n; assumption.
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni' ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni' ai a (NAtom i) *)
intros i' b n bs lookup nth; apply In_Atomic_Imps with n bs; assumption.
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros i' lookup; apply In_Atoms; assumption.
Qed.


Lemma in_ngamma_cons_ds_head :
 forall (work : nf_list) (i j : Int) (ds : disjs) (ni : nested_imps)
   (ai : atomic_imps) (a : atoms),
 in_ngamma work ((i, j) :: ds) ni ai a (NDisj i j).
(* Goal: forall (work : nf_list) (i j : Int) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms), in_ngamma work (@cons (prod Int Int) (@pair Int Int i j) ds) ni ai a (NDisj i j) *)
intros work i j ds ni ai a.
(* Goal: in_ngamma work (@cons (prod Int Int) (@pair Int Int i j) ds) ni ai a (NDisj i j) *)
apply In_Disjs with 0.
(* Goal: my_nth normal_form O (@cons normal_form b bs) b *)
apply My_NthO.
Qed.


Lemma in_ngamma_cons_ds_rev :
 forall (work : nf_list) (i j : Int) (ds : disjs) (ni : nested_imps)
   (ai : atomic_imps) (a : atoms) (c : normal_form),
 in_ngamma work ((i, j) :: ds) ni ai a c ->
 in_ngamma work ds ni ai a c + {c = NDisj i j}.
(* Goal: forall (work : nf_list) (i j : Int) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma work (@cons (prod Int Int) (@pair Int Int i j) ds) ni ai a c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NDisj i j)) *)
intros work i j ds ni ai a c in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
(* Goal: forall (n : nat) (i0 j : Int) (_ : my_nth disj n ds (@pair Int Int i0 j)), sumor (in_ngamma work ds ni ai a (NDisj i0 j)) (@eq normal_form (NDisj i0 j) (NAtom i)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) (NAtom i)) *)
(* Goal: forall (i0 : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i0 b)) (@eq normal_form (AImp i0 b) (NAtom i)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a' tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intros n c0 nth; left; apply In_Work with n; assumption.
(* Goal: forall (n : nat) (x0 : nimp) (_ : my_nth nimp n (nested_imps2nimps (@cons nested_imp x ni)) x0), sumor (in_ngamma work ds ni ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds ni ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros n; case n; clear n.
(* Goal: forall (i0 j0 : Int) (_ : my_nth disj O (@cons (prod Int Int) (@pair Int Int i j) ds) (@pair Int Int i0 j0)), sumor (in_ngamma work ds ni ai a (NDisj i0 j0)) (@eq normal_form (NDisj i0 j0) (NDisj i j)) *)
(* Goal: forall (n : nat) (i0 j0 : Int) (_ : my_nth disj (S n) (@cons (prod Int Int) (@pair Int Int i j) ds) (@pair Int Int i0 j0)), sumor (in_ngamma work ds ni ai a (NDisj i0 j0)) (@eq normal_form (NDisj i0 j0) (NDisj i j)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) (NDisj i j)) *)
(* Goal: forall (i0 : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i0 b)) (@eq normal_form (AImp i0 b) (NDisj i j)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NDisj i j)) *)
intros i' j' nth; right; inversion_clear nth; trivial.
intros n i' j' nth; left; apply In_Disjs with n; inversion_clear nth;
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
 assumption.
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) (AImp i b)) *)
(* Goal: forall (i0 : Int) (b0 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b0), sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros n x nth; left; apply In_Nested_Imps with n; assumption.
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds ni ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros i' b n bs lookup nth; left; apply In_Atomic_Imps with n bs; assumption.
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros i' lookup; left; apply In_Atoms; assumption.
Qed.


Lemma in_ngamma_cons_ni_tail :
 forall (work : nf_list) (ds : disjs) (x : nested_imp) 
   (ni : nested_imps) (ai : atomic_imps) (a : atoms) 
   (c : normal_form),
 in_ngamma work ds ni ai a c -> in_ngamma work ds (x :: ni) ai a c.
(* Goal: forall (work : nf_list) (ds : disjs) (x : nested_imp) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma work ds (@cons nested_imp x ni) ai a c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NImp_NF (nested_imp2nimp x))) *)
intros work ds x ni ai a c in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), in_ngamma work ds ni ai a' c *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni ai a' (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai a' (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai a' (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai a' (NAtom i) *)
intros n c0 nth; apply In_Work with n; assumption.
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni' ai a (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni' ai a (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni' ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni' ai a (NAtom i) *)
intros n i j nth; apply In_Disjs with n; assumption.
(* Goal: forall (n : nat) (x0 : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x0), in_ngamma work ds (@cons nested_imp x ni) ai a (NImp_NF x0) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds (@cons nested_imp x ni) ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@cons nested_imp x ni) ai a (NAtom i) *)
intros n x' nth; apply In_Nested_Imps with (S n).
(* Goal: my_nth nimp (S n') (nested_imps2nimps (@cons nested_imp x ni2)) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
simpl in |- *; apply My_NthS; assumption.
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni' ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni' ai a (NAtom i) *)
intros i' b n bs lookup nth; apply In_Atomic_Imps with n bs; assumption.
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros i' lookup; apply In_Atoms; assumption.
Qed.


Lemma in_ngamma_cons_ni_head :
 forall (work : nf_list) (ds : disjs) (x : nested_imp) 
   (ni : nested_imps) (ai : atomic_imps) (a : atoms),
 in_ngamma work ds (x :: ni) ai a (NImp_NF (nested_imp2nimp x)).
(* Goal: forall (work : nf_list) (ds : disjs) (x : nested_imp) (ni : nested_imps) (ai : atomic_imps) (a : atoms), in_ngamma work ds (@cons nested_imp x ni) ai a (NImp_NF (nested_imp2nimp x)) *)
intros work ds x ni ai a.
(* Goal: my_nth normal_form O (@cons normal_form b bs) b *)
apply In_Nested_Imps with 0; simpl in |- *; apply My_NthO.
Qed.

Lemma in_ngamma_cons_ni_rev :
 forall (work : nf_list) (ds : disjs) (x : nested_imp) 
   (ni : nested_imps) (ai : atomic_imps) (a : atoms) 
   (c : normal_form),
 in_ngamma work ds (x :: ni) ai a c ->
 in_ngamma work ds ni ai a c + {c = NImp_NF (nested_imp2nimp x)}.
(* Goal: forall (work : nf_list) (ds : disjs) (x : nested_imp) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma work ds (@cons nested_imp x ni) ai a c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NImp_NF (nested_imp2nimp x))) *)
intros work ds x ni ai a c in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), sumor (in_ngamma work ds ni ai a (NDisj i j)) (@eq normal_form (NDisj i j) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (n : nat) (x0 : nimp) (_ : my_nth nimp n (nested_imps2nimps (@cons nested_imp x ni)) x0), sumor (in_ngamma work ds ni ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds ni ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros n c1 nth; left; apply In_Work with n; assumption.
(* Goal: forall (n : nat) (i0 j : Int) (_ : my_nth disj n ds (@pair Int Int i0 j)), sumor (in_ngamma work ds ni ai a (NDisj i0 j)) (@eq normal_form (NDisj i0 j) (NAtom i)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) (NAtom i)) *)
(* Goal: forall (i0 : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i0 b)) (@eq normal_form (AImp i0 b) (NAtom i)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a' tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intros n i' j' nth; left; apply In_Disjs with n; assumption.
(* Goal: forall (n : nat) (x0 : nimp) (_ : my_nth nimp n (nested_imps2nimps (@cons nested_imp x ni)) x0), sumor (in_ngamma work ds ni ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds ni ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros n; case n; clear n.
(* Goal: forall (x0 : nimp) (_ : my_nth nimp O (nested_imps2nimps (@cons nested_imp x ni)) x0), sumor (in_ngamma work ds ni ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (n : nat) (x0 : nimp) (_ : my_nth nimp (S n) (nested_imps2nimps (@cons nested_imp x ni)) x0), sumor (in_ngamma work ds ni ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds ni ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros x' nth; right; inversion_clear nth; trivial.
intros n x' nth; left; apply In_Nested_Imps with n; inversion_clear nth;
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
 assumption.
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds ni ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros i' b n bs lookup nth; left; apply In_Atomic_Imps with n bs; assumption.
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros i' lookup; left; apply In_Atoms; assumption.
Qed.

Lemma in_ngamma_ni_x_ni_head :
 forall (work : nf_list) (ds : disjs) (x : nested_imp)
   (ni1 ni2 : nested_imps) (ai : atomic_imps) (a : atoms),
 in_ngamma work ds (ni1 ++ x :: ni2) ai a (NImp_NF (nested_imp2nimp x)).
(* Goal: forall (work : nf_list) (ds : disjs) (x : nested_imp) (ni1 ni2 : nested_imps) (ai : atomic_imps) (a : atoms), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NImp_NF (nested_imp2nimp x)) *)
intros work ds x ni1 ni2 ai a.
(* Goal: in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NImp_NF (nested_imp2nimp x)) *)
apply In_Nested_Imps with (n := length ni1) (x := nested_imp2nimp x).
(* Goal: my_nth nimp (Nat.add (@length nested_imp ni1) (S n')) (nested_imps2nimps (@app nested_imp ni1 (@cons nested_imp x ni2))) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
 rewrite (nested_imps2nimps_app ni1 (x :: ni2)).
(* Goal: my_nth nimp (Nat.add (@length nested_imp ni1) n') (nested_imps2nimps (@app nested_imp ni1 ni2)) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
 rewrite (nested_imps2nimps_length ni1).
(* Goal: my_nth nimp (@length nimp (nested_imps2nimps ni1)) (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) (nested_imp2nimp x) *)
 rewrite <- (plus_O (length (nested_imps2nimps ni1))).
(* Goal: my_nth nimp (Nat.add (@length nimp (nested_imps2nimps ni1)) n') (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
apply nth_app1.
(* Goal: my_nth normal_form O (@cons normal_form b bs) b *)
simpl in |- *; apply My_NthO.
Qed.


Lemma in_ngamma_ni_x_ni_tail :
 forall (work : nf_list) (ds : disjs) (x : nested_imp)
   (ni1 ni2 : nested_imps) (ai : atomic_imps) (a : atoms) 
   (c : normal_form),
 in_ngamma work ds (ni1 ++ ni2) ai a c ->
 in_ngamma work ds (ni1 ++ x :: ni2) ai a c.
(* Goal: forall (work : nf_list) (ds : disjs) (x : nested_imp) (ni1 ni2 : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a c), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a c) (@eq normal_form c (NImp_NF (nested_imp2nimp x))) *)
intros work ds x ni1 ni2 ai a c in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), in_ngamma work ds ni ai a' c *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni ai a' (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai a' (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai a' (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai a' (NAtom i) *)
intros n c0 nth; apply In_Work with n; assumption.
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni' ai a (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni' ai a (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni' ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni' ai a (NAtom i) *)
intros n i j nth; apply In_Disjs with n; assumption.
(* Goal: forall (n : nat) (x0 : nimp) (_ : my_nth nimp n (nested_imps2nimps (@app nested_imp ni1 (@cons nested_imp x ni2))) x0), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros n x0 nth.
(* Goal: in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NImp_NF x0) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
elim (inv_nth_app nimp n (nested_imps2nimps ni1) (nested_imps2nimps ni2) x0).
(* Goal: forall _ : my_nth nimp n (nested_imps2nimps ni1) x0, in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NImp_NF x0) *)
(* Goal: forall (n' : nat) (_ : my_nth nimp n' (nested_imps2nimps ni2) x0), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NImp_NF x0) *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
intros nth'; apply In_Nested_Imps with n.
(* Goal: my_nth nimp (Nat.add (@length nested_imp ni1) (S n')) (nested_imps2nimps (@app nested_imp ni1 (@cons nested_imp x ni2))) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
 rewrite (nested_imps2nimps_app ni1 (x :: ni2)).
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) x0 *)
(* Goal: forall (n' : nat) (_ : my_nth nimp n' (nested_imps2nimps (@cons nested_imp x ni2)) x0), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
apply nth_app0; assumption.
(* Goal: forall (n' : nat) (_ : my_nth nimp n' (nested_imps2nimps ni2) x0), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NImp_NF x0) *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
intros n' nth'; apply In_Nested_Imps with (length ni1 + S n').
(* Goal: my_nth nimp (Nat.add (@length nested_imp ni1) (S n')) (nested_imps2nimps (@app nested_imp ni1 (@cons nested_imp x ni2))) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
 rewrite (nested_imps2nimps_app ni1 (x :: ni2)).
(* Goal: my_nth nimp (Nat.add (@length nested_imp ni1) n') (nested_imps2nimps (@app nested_imp ni1 ni2)) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
 rewrite (nested_imps2nimps_length ni1).
(* Goal: my_nth nimp (Nat.add (@length nimp (nested_imps2nimps ni1)) n') (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
apply nth_app1.
(* Goal: my_nth nimp (S n') (nested_imps2nimps (@cons nested_imp x ni2)) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
simpl in |- *; apply My_NthS; assumption.
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
 rewrite <- (nested_imps2nimps_app ni1 ni2); assumption.
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
intros i b n bs lookup nth; apply In_Atomic_Imps with n bs; assumption.
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NAtom i) *)
intros i lookup; apply In_Atoms; assumption.
Qed.


Lemma in_ngamma_ni_x_ni_rev :
 forall (work : nf_list) (ds : disjs) (x : nested_imp)
   (ni1 ni2 : nested_imps) (ai : atomic_imps) (a : atoms) 
   (c : normal_form),
 in_ngamma work ds (ni1 ++ x :: ni2) ai a c ->
 in_ngamma work ds (ni1 ++ ni2) ai a c + {c = NImp_NF (nested_imp2nimp x)}.
(* Goal: forall (work : nf_list) (ds : disjs) (x : nested_imp) (ni1 ni2 : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a c), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a c) (@eq normal_form c (NImp_NF (nested_imp2nimp x))) *)
intros work ds x ni1 ni2 ai a c in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
(* Goal: forall (n : nat) (i0 j : Int) (_ : my_nth disj n ds (@pair Int Int i0 j)), sumor (in_ngamma work ds ni ai a (NDisj i0 j)) (@eq normal_form (NDisj i0 j) (NAtom i)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) (NAtom i)) *)
(* Goal: forall (i0 : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i0 b)) (@eq normal_form (AImp i0 b) (NAtom i)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a' tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intros n c0 nth; left; apply In_Work with n; assumption.
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NDisj i j)) (@eq normal_form (NDisj i j) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (n : nat) (x0 : nimp) (_ : my_nth nimp n (nested_imps2nimps (@app nested_imp ni1 (@cons nested_imp x ni2))) x0), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros n i j nth; left; apply In_Disjs with n; assumption.
(* Goal: forall (n : nat) (x0 : nimp) (_ : my_nth nimp n (nested_imps2nimps (@app nested_imp ni1 (@cons nested_imp x ni2))) x0), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros n x0 nth.
elim
 (inv_nth_app nimp n (nested_imps2nimps ni1) (nested_imps2nimps (x :: ni2))
    x0).
(* Goal: forall _ : my_nth nimp n (nested_imps2nimps ni1) x0, sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (n' : nat) (_ : my_nth nimp n' (nested_imps2nimps (@cons nested_imp x ni2)) x0), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros n0; left; apply In_Nested_Imps with n.

(* Goal: my_nth nimp (Nat.add (@length nimp (nested_imps2nimps ni1)) n') (nested_imps2nimps (@app nested_imp ni1 ni2)) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
 rewrite (nested_imps2nimps_app ni1 ni2).
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) x0 *)
(* Goal: forall (n' : nat) (_ : my_nth nimp n' (nested_imps2nimps (@cons nested_imp x ni2)) x0), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
apply nth_app0; assumption.
(* Goal: forall (n' : nat) (_ : my_nth nimp n' (nested_imps2nimps (@cons nested_imp x ni2)) x0), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros n'; case n'; clear n'.
(* Goal: forall _ : my_nth nimp O (nested_imps2nimps (@cons nested_imp x ni2)) x0, sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (n : nat) (_ : my_nth nimp (S n) (nested_imps2nimps (@cons nested_imp x ni2)) x0), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros nth'; right; inversion_clear nth'; trivial.
(* Goal: forall (n : nat) (_ : my_nth nimp (S n) (nested_imps2nimps (@cons nested_imp x ni2)) x0), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NImp_NF x0)) (@eq normal_form (NImp_NF x0) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros n' nth'; left; apply In_Nested_Imps with (length ni1 + n').
(* Goal: my_nth nimp (Nat.add (@length nested_imp ni1) n') (nested_imps2nimps (@app nested_imp ni1 ni2)) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
 rewrite (nested_imps2nimps_length ni1).
(* Goal: my_nth nimp (Nat.add (@length nimp (nested_imps2nimps ni1)) n') (nested_imps2nimps (@app nested_imp ni1 ni2)) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
 rewrite (nested_imps2nimps_app ni1 ni2).
(* Goal: my_nth nimp (Nat.add (@length nimp (nested_imps2nimps ni1)) n') (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps ni2)) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
apply nth_app1.
(* Goal: my_nth nimp n' (nested_imps2nimps ni2) x0 *)
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
inversion_clear nth'; assumption.
(* Goal: my_nth nimp n (@app nimp (nested_imps2nimps ni1) (nested_imps2nimps (@cons nested_imp x ni2))) x0 *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
 rewrite <- (nested_imps2nimps_app ni1 (x :: ni2)); assumption.
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (AImp i b)) (@eq normal_form (AImp i b) (NImp_NF (nested_imp2nimp x))) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros i b n bs lookup nth; left; apply In_Atomic_Imps with n bs; assumption.
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), sumor (in_ngamma work ds (@app nested_imp ni1 ni2) ai a (NAtom i)) (@eq normal_form (NAtom i) (NImp_NF (nested_imp2nimp x))) *)
intros i lookup; left; apply In_Atoms; assumption.
Qed.



Lemma in_ngamma_ni_eq :
 forall (work : nf_list) (ds : disjs) (ni ni' : nested_imps)
   (ai : atomic_imps) (a : atoms) (c : normal_form),
 nested_imps2nimps ni = nested_imps2nimps ni' ->
 in_ngamma work ds ni ai a c -> in_ngamma work ds ni' ai a c.
(* Goal: forall (work : nf_list) (ds : disjs) (ni ni' : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : @eq (list nimp) (nested_imps2nimps ni) (nested_imps2nimps ni')) (_ : in_ngamma work ds ni ai a c), in_ngamma work ds ni' ai a c *)
intros work ds ni ni' ai a c eq in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), in_ngamma work ds ni ai a' c *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni ai a' (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai a' (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai a' (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai a' (NAtom i) *)
intros n c0 nth; apply In_Work with n; assumption.
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni' ai a (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni' ai a (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni' ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni' ai a (NAtom i) *)
intros n i j nth; apply In_Disjs with n; assumption.
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni' ai a (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni' ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni' ai a (NAtom i) *)
intros n x' nth; apply In_Nested_Imps with n.
(* Goal: my_nth nimp n (nested_imps2nimps ni') x' *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni' ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni' ai a (NAtom i) *)
 rewrite <- eq; assumption.
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni' ai a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni' ai a (NAtom i) *)
intros i' b n bs lookup nth; apply In_Atomic_Imps with n bs; assumption.
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros i' lookup; apply In_Atoms; assumption.
Qed.


Lemma in_ngamma_ins_ai_tail :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (i : Int) (b : normal_form) (ai ai' : atomic_imps) 
   (a : atoms) (c : normal_form),
 EQUIV_INS nf_list i (cons b) nf_nil ai ai' ->
 in_ngamma work ds ni ai a c -> in_ngamma work ds ni ai' a c.
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (i : Int) (b : normal_form) (ai ai' : atomic_imps) (a : atoms) (c : normal_form) (_ : EQUIV_INS nf_list i (@cons normal_form b) nf_nil ai ai') (_ : in_ngamma work ds ni ai' a c), in_ngamma (@cons normal_form (AImp i b) work) ds ni ai a c *)
intros work ds ni i b ai ai' a c equiv_ins in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), in_ngamma work ds ni ai a' c *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni ai a' (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai a' (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai a' (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai a' (NAtom i) *)
intros n c0 nth; apply In_Work with n; assumption.
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni ai a' (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai a' (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai a' (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai a' (NAtom i) *)
intros n i' j' nth; apply In_Disjs with n; assumption.
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai' a (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai' a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros n x nth; apply In_Nested_Imps with n; assumption.
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai' a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros i0 b0 n bs lookup nth. 
(* Goal: AvlTrees.lookup unit i0 t' tt *)
case (equal_dec i0 i).
(* Goal: forall _ : Equal i0 i, in_ngamma work ds ni ai' a (AImp i0 b0) *)
(* Goal: forall _ : not (Equal i0 i), in_ngamma work ds ni ai' a (AImp i0 b0) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intro equal_i0_i.
(* Goal: in_ngamma work ds ni ai' a (AImp i0 b0) *)
(* Goal: forall _ : not (Equal i0 i), in_ngamma work ds ni ai' a (AImp i0 b0) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
apply In_Atomic_Imps with (S n) (b :: bs).
(* Goal: LOOKUP unit i0 a tt *)
generalize equiv_ins lookup; clear equiv_ins lookup.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' ai) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 ai bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai; clear ai; intros t avl_t.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' (AVL_intro nf_list t avl_t)) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 (AVL_intro nf_list t avl_t) bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai'; clear ai'; intros t' avl_t'.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: forall (_ : equiv_ins nf_list i (@cons normal_form b) nf_nil t t') (_ : lookup nf_list i0 t' bs), lookup nf_list i0 t bs *)
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros equiv_ins lookup.
(* Goal: AvlTrees.lookup unit i0 t tt *)
inversion_clear equiv_ins.
(* Goal: AvlTrees.lookup nf_list i0 t' (@cons normal_form b bs) *)
(* Goal: my_nth normal_form (S n) (@cons normal_form b bs) b0 *)
(* Goal: forall _ : not (Equal i0 i), in_ngamma work ds ni ai' a (AImp i0 b0) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
apply H; assumption.
(* Goal: my_nth normal_form (S n) (@cons normal_form b bs) b0 *)
(* Goal: forall _ : not (Equal i0 i), in_ngamma work ds ni ai' a (AImp i0 b0) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
apply My_NthS; assumption.
(* Goal: forall _ : not (Equal i0 i), in_ngamma work ds ni ai' a (AImp i0 b0) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros not_equal_i0_i.
(* Goal: in_ngamma work ds ni ai' a (AImp i0 b0) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
apply In_Atomic_Imps with n bs.
(* Goal: LOOKUP unit i0 a tt *)
generalize equiv_ins lookup; clear equiv_ins lookup.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' ai) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 ai bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai; clear ai; intros t avl_t.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' (AVL_intro nf_list t avl_t)) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 (AVL_intro nf_list t avl_t) bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai'; clear ai'; intros t' avl_t'.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: forall (_ : equiv_ins nf_list i (@cons normal_form b) nf_nil t t') (_ : lookup nf_list i0 t' bs), lookup nf_list i0 t bs *)
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros equiv_ins lookup.
(* Goal: AvlTrees.lookup unit i0 t tt *)
inversion_clear equiv_ins.
(* Goal: AvlTrees.lookup unit i0 t' tt *)
apply H1; assumption.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
assumption.
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros i' lookup; apply In_Atoms; assumption.
Qed.



Lemma in_ngamma_ins_ai_head_new :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (i : Int) (b : normal_form) (ai ai' : atomic_imps) 
   (a : atoms),
 (forall bs : nf_list, LOOKUP nf_list i ai bs -> False) ->
 EQUIV_INS nf_list i (cons b) nf_nil ai ai' ->
 in_ngamma work ds ni ai' a (AImp i b).
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (i : Int) (b : normal_form) (ai ai' : atomic_imps) (a : atoms) (_ : forall (bs : nf_list) (_ : LOOKUP nf_list i ai bs), False) (_ : EQUIV_INS nf_list i (@cons normal_form b) nf_nil ai ai'), in_ngamma work ds ni ai' a (AImp i b) *)
intros work ds ni i b ai ai' a notlookup equiv_ins.
(* Goal: in_ngamma work ds ni ai' a (AImp i b) *)
apply In_Atomic_Imps with 0 (b :: nf_nil).
(* Goal: LOOKUP nf_list i ai' (@cons normal_form b nf_nil) *)
(* Goal: my_nth normal_form O (@cons normal_form b nf_nil) b *)
generalize equiv_ins notlookup; clear equiv_ins notlookup.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' ai) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 ai bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai; clear ai; intros t avl_t.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' (AVL_intro nf_list t avl_t)) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 (AVL_intro nf_list t avl_t) bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai'; clear ai'; intros t' avl_t'.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: forall (_ : forall d : unit, not (lookup unit i t d)) (_ : equiv_ins unit i (fun _ : unit => tt) tt t t'), lookup unit i t' tt *)
intros.
(* Goal: AvlTrees.lookup unit i0 t tt *)
inversion_clear equiv_ins.
(* Goal: AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
clear H1 H2.
(* Goal: lookup unit i t' tt *)
apply H0.
(* Goal: Equal i i *)
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply equal_refl.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
assumption.
(* Goal: my_nth normal_form O (@cons normal_form b bs) b *)
apply My_NthO.
Qed.


Lemma in_ngamma_ins_ai_head_old :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (i : Int) (b : normal_form) (bs : nf_list) (ai ai' : atomic_imps)
   (a : atoms),
 LOOKUP nf_list i ai bs ->
 EQUIV_INS nf_list i (cons b) nf_nil ai ai' ->
 in_ngamma work ds ni ai' a (AImp i b).
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (i : Int) (b : normal_form) (bs : nf_list) (ai ai' : atomic_imps) (a : atoms) (_ : LOOKUP nf_list i ai bs) (_ : EQUIV_INS nf_list i (@cons normal_form b) nf_nil ai ai'), in_ngamma work ds ni ai' a (AImp i b) *)
intros work ds ni i b bs ai ai' a lookup equiv_ins.
(* Goal: in_ngamma work ds ni ai' a (AImp i b) *)
apply In_Atomic_Imps with 0 (b :: bs).
(* Goal: LOOKUP unit i0 a tt *)
generalize equiv_ins lookup; clear equiv_ins lookup.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' ai) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 ai bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai; clear ai; intros t avl_t.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' (AVL_intro nf_list t avl_t)) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 (AVL_intro nf_list t avl_t) bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai'; clear ai'; intros t' avl_t'.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: forall (_ : forall d : unit, not (lookup unit i t d)) (_ : equiv_ins unit i (fun _ : unit => tt) tt t t'), lookup unit i t' tt *)
intros.
(* Goal: AvlTrees.lookup unit i0 t tt *)
inversion_clear equiv_ins.
(* Goal: AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
clear H1 H2.
(* Goal: AvlTrees.lookup nf_list i t' (@cons normal_form b bs) *)
(* Goal: my_nth normal_form O (@cons normal_form b bs) b *)
apply H. 
(* Goal: Equal i i *)
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply equal_refl.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
assumption.
(* Goal: my_nth normal_form O (@cons normal_form b bs) b *)
apply My_NthO.
Qed.




Lemma in_ngamma_ins_ai_rev :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (i : Int) (b : normal_form) (ai ai' : atomic_imps) 
   (a : atoms) (c : normal_form),
 EQUIV_INS nf_list i (cons b) nf_nil ai ai' ->
 in_ngamma work ds ni ai' a c -> in_ngamma work ds ni ai a c + {c = AImp i b}.
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (i : Int) (b : normal_form) (ai ai' : atomic_imps) (a : atoms) (c : normal_form) (_ : EQUIV_INS nf_list i (@cons normal_form b) nf_nil ai ai') (_ : in_ngamma work ds ni ai' a c), in_ngamma (@cons normal_form (AImp i b) work) ds ni ai a c *)
intros work ds ni i b ai ai' a c equiv_ins in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
intros n c0; left; apply In_Work with n; assumption.
(* Goal: forall (n : nat) (i0 j : Int) (_ : my_nth disj n ds (@pair Int Int i0 j)), sumor (in_ngamma work ds ni ai a (NDisj i0 j)) (@eq normal_form (NDisj i0 j) (NAtom i)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) (NAtom i)) *)
(* Goal: forall (i0 : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i0 b)) (@eq normal_form (AImp i0 b) (NAtom i)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a' tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intros n i' j' nth; left; apply In_Disjs with n; assumption.
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) (AImp i b)) *)
(* Goal: forall (i0 : Int) (b0 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b0), sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros n x nth; left; apply In_Nested_Imps with n; assumption.
(* Goal: forall (i0 : Int) (b0 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b0), sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros i0.
(* Goal: sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
elim (equal_dec i0 i).
(* Goal: forall _ : Equal i0 i, sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
(* Goal: forall _ : not (Equal i0 i), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intro equal.
(* Goal: forall (b0 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b0), sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros b0 n. 
(* Goal: forall (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b0), sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
case n; clear n.
(* Goal: forall (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form O bs b0), sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form (S n) bs b0), sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros bs lookup nth.
(* Goal: sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
(* Goal: forall _ : not (Equal i0 i), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
right.
(* Goal: LOOKUP unit i0 a tt *)
generalize equiv_ins lookup; clear equiv_ins lookup.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' ai) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 ai bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai; clear ai; intros t avl_t.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' (AVL_intro nf_list t avl_t)) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 (AVL_intro nf_list t avl_t) bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai'; clear ai'; intros t' avl_t'.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: forall (_ : equiv_ins nf_list i (@cons normal_form b) nf_nil t t') (_ : lookup nf_list i0 t' bs), lookup nf_list i0 t bs *)
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros equiv_ins lookup.
(* Goal: AvlTrees.lookup unit i0 t tt *)
inversion_clear equiv_ins.
(* Goal: AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
clear H1 H2.
(* Goal: AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
elim (lookup_dec nf_list i0 t avl_t).
(* Goal: forall (d : nf_list) (_ : AvlTrees.lookup nf_list i0 t d), AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: forall _ : forall d : nf_list, not (AvlTrees.lookup nf_list i0 t d), AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros bs' lookup0.
(* Goal: AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: forall _ : forall d : nf_list, not (AvlTrees.lookup nf_list i0 t d), AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
generalize (H i0 bs' equal lookup0); clear H H0.
(* Goal: forall (_ : forall d : unit, not (lookup unit i t d)) (_ : equiv_ins unit i (fun _ : unit => tt) tt t t'), lookup unit i t' tt *)
intros.
 rewrite (lookup_avl_equal nf_list i0 i0 t' bs (b :: bs')) in nth;
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
 try assumption.
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
inversion_clear nth.
(* Goal: @eq normal_form (AImp i0 b0) (AImp i b0) *)
(* Goal: Equal i0 i0 *)
(* Goal: forall (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form (S n) bs b0), sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
 rewrite (equal_eq i0 i).
(* Goal: @eq normal_form (AImp i b0) (AImp i b0) *)
(* Goal: forall _ : not (Equal i0 i), sum (in_ngamma work ds ni ai a (AImp i0 b0)) (in_ngamma_del_ai_rev_spec i bs (AImp i0 b0)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
trivial.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
assumption.
(* Goal: Equal i i *)
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply equal_refl.
(* Goal: forall _ : forall d : nf_list, not (AvlTrees.lookup nf_list i0 t d), AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros notlookup0.
(* Goal: AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
generalize (H0 i0 equal notlookup0); clear H H0.
(* Goal: forall (_ : forall d : unit, not (lookup unit i t d)) (_ : equiv_ins unit i (fun _ : unit => tt) tt t t'), lookup unit i t' tt *)
intros.
 rewrite (lookup_avl_equal nf_list i0 i0 t' bs (b :: nf_nil)) in nth;
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
 try assumption.
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
inversion_clear nth.
(* Goal: @eq normal_form (AImp i0 b0) (AImp i b0) *)
(* Goal: Equal i0 i0 *)
(* Goal: forall (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form (S n) bs b0), sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
 rewrite (equal_eq i0 i).
(* Goal: @eq normal_form (AImp i b0) (AImp i b0) *)
(* Goal: forall _ : not (Equal i0 i), sum (in_ngamma work ds ni ai a (AImp i0 b0)) (in_ngamma_del_ai_rev_spec i bs (AImp i0 b0)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
trivial.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
assumption.
(* Goal: Equal i i *)
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply equal_refl.
(* Goal: forall (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form (S n) bs b0), sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros n bs lookup nth.
(* Goal: sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
left; apply In_Atomic_Imps with n (tail bs).
(* Goal: LOOKUP unit i0 a tt *)
generalize equiv_ins lookup; clear equiv_ins lookup.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' ai) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 ai bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai; clear ai; intros t avl_t.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' (AVL_intro nf_list t avl_t)) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 (AVL_intro nf_list t avl_t) bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai'; clear ai'; intros t' avl_t'.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: forall (_ : equiv_ins nf_list i (@cons normal_form b) nf_nil t t') (_ : lookup nf_list i0 t' bs), lookup nf_list i0 t bs *)
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros equiv_ins lookup.
(* Goal: AvlTrees.lookup unit i0 t tt *)
inversion_clear equiv_ins.
(* Goal: AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
clear H1 H2.
(* Goal: AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
elim (lookup_dec nf_list i0 t avl_t).
(* Goal: forall (d : nf_list) (_ : AvlTrees.lookup nf_list i0 t d), AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: forall _ : forall d : nf_list, not (AvlTrees.lookup nf_list i0 t d), AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros bs' lookup0.
(* Goal: AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: forall _ : forall d : nf_list, not (AvlTrees.lookup nf_list i0 t d), AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
generalize (H i0 bs' equal lookup0); clear H H0.
(* Goal: forall (_ : forall d : unit, not (lookup unit i t d)) (_ : equiv_ins unit i (fun _ : unit => tt) tt t t'), lookup unit i t' tt *)
intros.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
 rewrite (lookup_avl_equal nf_list i0 i0 t' bs (b :: bs')); try assumption.
(* Goal: Equal i i *)
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply equal_refl.
(* Goal: forall _ : forall d : nf_list, not (AvlTrees.lookup nf_list i0 t d), AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros notlookup0.
(* Goal: AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
generalize (H0 i0 equal notlookup0); clear H H0.
(* Goal: forall (_ : forall d : unit, not (lookup unit i t d)) (_ : equiv_ins unit i (fun _ : unit => tt) tt t t'), lookup unit i t' tt *)
intros.
 rewrite (lookup_avl_equal nf_list i0 i0 t' bs (b :: nf_nil)) in nth;
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
 try assumption.
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
inversion_clear nth.
(* Goal: AvlTrees.lookup nf_list i0 t (@tl normal_form bs) *)
(* Goal: Equal i0 i0 *)
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
inversion_clear H0.
(* Goal: Equal i i *)
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply equal_refl.
(* Goal: my_nth normal_form n (@tl normal_form bs) b0 *)
(* Goal: forall (_ : not (Equal i0 i)) (b1 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b1), sumor (in_ngamma work ds ni ai a (AImp i0 b1)) (@eq normal_form (AImp i0 b1) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
inversion_clear nth.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
assumption.

(* Goal: forall _ : not (Equal i0 i), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intros notequal.
(* Goal: forall (b0 : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai' bs) (_ : my_nth normal_form n bs b0), sumor (in_ngamma work ds ni ai a (AImp i0 b0)) (@eq normal_form (AImp i0 b0) (AImp i b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros b0 n bs lookup nth.
(* Goal: in_ngamma work ds ni ai' a (AImp i0 b0) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
left; apply In_Atomic_Imps with n bs.
(* Goal: LOOKUP unit i0 a tt *)
generalize equiv_ins lookup; clear equiv_ins lookup.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' ai) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 ai bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai; clear ai; intros t avl_t.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' (AVL_intro nf_list t avl_t)) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 (AVL_intro nf_list t avl_t) bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai'; clear ai'; intros t' avl_t'.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: forall (_ : equiv_ins nf_list i (@cons normal_form b) nf_nil t t') (_ : lookup nf_list i0 t' bs), lookup nf_list i0 t bs *)
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros equiv_ins lookup.
(* Goal: AvlTrees.lookup unit i0 t tt *)
inversion_clear equiv_ins.
(* Goal: AvlTrees.lookup nf_list i0 t bs *)
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
clear H H0.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply H2; assumption.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
assumption.
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
intros i' lookup; left; apply In_Atoms; assumption.
Qed.




Lemma in_ngamma_del_ai_tail :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (i : Int) (ai ai' : atomic_imps) (a : atoms) (c : normal_form),
 EQUIV_DEL nf_list i ai' ai ->
 in_ngamma work ds ni ai a c -> in_ngamma work ds ni ai' a c.
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (i : Int) (ai ai' : atomic_imps) (a : atoms) (c : normal_form) (_ : EQUIV_DEL nf_list i ai' ai) (_ : in_ngamma work ds ni ai a c), in_ngamma work ds ni ai' a c *)
intros work ds ni i ai ai' a c equiv_del in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), in_ngamma work ds ni ai a' c *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni ai a' (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai a' (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai a' (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai a' (NAtom i) *)
intros n c0 nth; apply In_Work with n; assumption.
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni ai a' (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai a' (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai a' (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai a' (NAtom i) *)
intros n i' j' nth; apply In_Disjs with n; assumption.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
intros n x' nth; apply In_Nested_Imps with n; assumption.
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai' a (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros i0 b0 n bs lookup nth. 
(* Goal: in_ngamma work ds ni ai' a (AImp i0 b0) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
apply In_Atomic_Imps with n bs.
(* Goal: LOOKUP nf_list i0 ai' bs *)
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
generalize equiv_del lookup; clear equiv_del lookup.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' ai) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 ai bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai; clear ai; intros t avl_t.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' (AVL_intro nf_list t avl_t)) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 (AVL_intro nf_list t avl_t) bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai'; clear ai'; intros t' avl_t'.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: forall (_ : equiv_del nf_list i t' t) (_ : lookup nf_list i0 t bs), lookup nf_list i0 t' bs *)
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros equiv_del lookup.
(* Goal: AvlTrees.lookup nf_list i0 t bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
inversion_clear equiv_del.
(* Goal: sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
elim (equal_dec i0 i).
(* Goal: forall _ : Equal i0 i, sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
(* Goal: forall _ : not (Equal i0 i), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intro equal.
(* Goal: AvlTrees.lookup nf_list i0 t' bs *)
(* Goal: forall _ : not (Equal i0 i), AvlTrees.lookup nf_list i0 t' bs *)
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
elimtype False.
(* Goal: False *)
(* Goal: forall _ : not (Equal i0 i), AvlTrees.lookup nf_list i0 t' bs *)
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
apply (H i0 equal bs lookup).
(* Goal: forall _ : not (Equal i0 i), AvlTrees.lookup nf_list i0 t' bs *)
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros not_equal.
(* Goal: AvlTrees.lookup unit i0 t' tt *)
apply H1; assumption.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
assumption.

(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai' a (NAtom i) *)
intros i' lookup; apply In_Atoms; assumption.
Qed.


Inductive in_ngamma_del_ai_rev_spec (i : Int) (bs : nf_list)
(c : normal_form) : Set :=
    In_NGamma_Del_AI_Rev_Spec_Intro :
      forall (b : normal_form) (n : nat),
      my_nth normal_form n bs b ->
      c = AImp i b -> in_ngamma_del_ai_rev_spec i bs c.


Lemma in_ngamma_del_ai_rev :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (i : Int) (bs : nf_list) (ai ai' : atomic_imps) 
   (a : atoms) (c : normal_form),
 LOOKUP nf_list i ai' bs ->
 EQUIV_DEL nf_list i ai' ai ->
 in_ngamma work ds ni ai' a c ->
 in_ngamma work ds ni ai a c + in_ngamma_del_ai_rev_spec i bs c.
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (i : Int) (bs : nf_list) (ai ai' : atomic_imps) (a : atoms) (c : normal_form) (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' ai) (_ : in_ngamma work ds ni ai' a c), sum (in_ngamma work ds ni ai a c) (in_ngamma_del_ai_rev_spec i bs c) *)
intros work ds ni i bs ai ai' a c lookup equiv_del in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
(* Goal: forall (n : nat) (i0 j : Int) (_ : my_nth disj n ds (@pair Int Int i0 j)), sumor (in_ngamma work ds ni ai a (NDisj i0 j)) (@eq normal_form (NDisj i0 j) (NAtom i)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) (NAtom i)) *)
(* Goal: forall (i0 : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i0 b)) (@eq normal_form (AImp i0 b) (NAtom i)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a' tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intros n c0 nth; left; apply In_Work with n; assumption.
(* Goal: forall (n : nat) (i0 j : Int) (_ : my_nth disj n ds (@pair Int Int i0 j)), sumor (in_ngamma work ds ni ai a (NDisj i0 j)) (@eq normal_form (NDisj i0 j) (NAtom i)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) (NAtom i)) *)
(* Goal: forall (i0 : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i0 b)) (@eq normal_form (AImp i0 b) (NAtom i)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a' tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intros n i' j' nth; left; apply In_Disjs with n; assumption.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
intros n x' nth; left; apply In_Nested_Imps with n; assumption.
(* Goal: forall (i0 : Int) (b : normal_form) (n : nat) (bs0 : nf_list) (_ : LOOKUP nf_list i0 ai' bs0) (_ : my_nth normal_form n bs0 b), sum (in_ngamma work ds ni ai a (AImp i0 b)) (in_ngamma_del_ai_rev_spec i bs (AImp i0 b)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
intros i0 b0 n bs0 lookup0 nth. 
(* Goal: sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
elim (equal_dec i0 i).
(* Goal: forall _ : Equal i0 i, sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
(* Goal: forall _ : not (Equal i0 i), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intro equal.
(* Goal: sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
(* Goal: forall _ : not (Equal i0 i), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
right.
(* Goal: in_ngamma_del_ai_rev_spec i bs (AImp i0 b0) *)
(* Goal: forall _ : not (Equal i0 i), sum (in_ngamma work ds ni ai a (AImp i0 b0)) (in_ngamma_del_ai_rev_spec i bs (AImp i0 b0)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
 rewrite (equal_eq i0 i equal).
(* Goal: in_ngamma_del_ai_rev_spec i bs (AImp i b0) *)
(* Goal: forall _ : not (Equal i0 i), sum (in_ngamma work ds ni ai a (AImp i0 b0)) (in_ngamma_del_ai_rev_spec i bs (AImp i0 b0)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
exists b0 n.
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: @eq normal_form (AImp i b0) (AImp i b0) *)
(* Goal: forall _ : not (Equal i0 i), sum (in_ngamma work ds ni ai a (AImp i0 b0)) (in_ngamma_del_ai_rev_spec i bs (AImp i0 b0)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
generalize equiv_del lookup0 lookup; clear equiv_del lookup0 lookup.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' ai) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 ai bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai; clear ai; intros t avl_t.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' (AVL_intro nf_list t avl_t)) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 (AVL_intro nf_list t avl_t) bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai'; clear ai'; intros t' avl_t'.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: forall (_ : forall d : unit, not (lookup unit i t d)) (_ : equiv_ins unit i (fun _ : unit => tt) tt t t'), lookup unit i t' tt *)
intros.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
 rewrite <- (lookup_avl_equal nf_list i0 i t' bs0 bs); try assumption.
(* Goal: @eq normal_form (AImp i b0) (AImp i b0) *)
(* Goal: forall _ : not (Equal i0 i), sum (in_ngamma work ds ni ai a (AImp i0 b0)) (in_ngamma_del_ai_rev_spec i bs (AImp i0 b0)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
trivial.
(* Goal: forall _ : not (Equal i0 i), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intros notequal.
(* Goal: sum (in_ngamma work ds ni ai a (AImp i0 b0)) (in_ngamma_del_ai_rev_spec i bs (AImp i0 b0)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
left.
(* Goal: in_ngamma work ds ni ai a (AImp i0 b0) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
apply In_Atomic_Imps with n bs0.
(* Goal: LOOKUP nf_list i0 ai bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
generalize lookup equiv_del lookup0; clear lookup equiv_del lookup0.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' ai) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 ai bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai; clear ai; intros t avl_t.
(* Goal: forall (_ : LOOKUP nf_list i ai' bs) (_ : EQUIV_DEL nf_list i ai' (AVL_intro nf_list t avl_t)) (_ : LOOKUP nf_list i0 ai' bs0), LOOKUP nf_list i0 (AVL_intro nf_list t avl_t) bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
elim ai'; clear ai'; intros t' avl_t'.
(* Goal: forall (_ : forall d : unit, not (lookup unit i t d)) (_ : equiv_ins unit i (fun _ : unit => tt) tt t t'), lookup unit i t' tt *)
simpl in |- *; intros.
(* Goal: AvlTrees.lookup nf_list i0 t bs0 *)
(* Goal: my_nth normal_form n bs0 b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
inversion_clear equiv_del.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply H0; assumption.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
assumption.

(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
intros i' lookup'; left; apply In_Atoms; assumption.
Qed.




Lemma in_ngamma_ins_a_tail :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (ai : atomic_imps) (i : Int) (a a' : atoms) (c : normal_form),
 EQUIV_INS unit i (fun _ : unit => tt) tt a a' ->
 in_ngamma work ds ni ai a c -> in_ngamma work ds ni ai a' c.
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (i : Int) (a a' : atoms) (c : normal_form) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a') (_ : in_ngamma work ds ni ai a' c), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros work ds ni ai i a a' c equiv_ins in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), in_ngamma work ds ni ai a' c *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni ai a' (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai a' (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai a' (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai a' (NAtom i) *)
intros n c0 nth; apply In_Work with n; assumption.
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n ds (@pair Int Int i j)), in_ngamma work ds ni ai a' (NDisj i j) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), in_ngamma work ds ni ai a' (NImp_NF x) *)
(* Goal: forall (i : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i ai bs) (_ : my_nth normal_form n bs b), in_ngamma work ds ni ai a' (AImp i b) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), in_ngamma work ds ni ai a' (NAtom i) *)
intros n i' j' nth; apply In_Disjs with n; assumption.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
intros n x' nth; apply In_Nested_Imps with n; assumption.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
intros i0 b0 n bs lookup nth; apply In_Atomic_Imps with n bs; assumption.

(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a' tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intros i0 lookup. 
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
apply In_Atoms.
(* Goal: LOOKUP unit i0 a tt *)
generalize equiv_ins lookup; clear equiv_ins lookup.
(* Goal: forall (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a') (_ : LOOKUP unit i0 a' tt), LOOKUP unit i0 a tt *)
elim a; clear a; intros t avl_t.
(* Goal: forall (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit t avl_t) a') (_ : LOOKUP unit i0 a' tt), LOOKUP unit i0 (AVL_intro unit t avl_t) tt *)
elim a'; clear a'; intros t' avl_t'.
(* Goal: forall (_ : equiv_ins nf_list i (@cons normal_form b) nf_nil t t') (_ : lookup nf_list i0 t' bs), lookup nf_list i0 t bs *)
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
simpl in |- *; intros equiv_ins lookup.
(* Goal: AvlTrees.lookup unit i0 t tt *)
inversion_clear equiv_ins.
(* Goal: AvlTrees.lookup unit i0 t' tt *)
case (equal_dec i0 i).
(* Goal: forall _ : Equal i0 i, sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
(* Goal: forall _ : not (Equal i0 i), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intro equal.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply H with tt; assumption.
(* Goal: forall _ : not (Equal i0 i), AvlTrees.lookup unit i0 t' tt *)
intro notequal.
(* Goal: AvlTrees.lookup unit i0 t' tt *)
apply H1; assumption.
Qed.



Lemma in_ngamma_ins_a_head :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (ai : atomic_imps) (i : Int) (a a' : atoms),
 EQUIV_INS unit i (fun _ : unit => tt) tt a a' ->
 in_ngamma work ds ni ai a' (NAtom i).
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (i : Int) (a a' : atoms) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a'), in_ngamma work ds ni ai a' (NAtom i) *)
intros work ds ni ai i a a' equiv_ins.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
apply In_Atoms.
(* Goal: LOOKUP unit i a' tt *)
generalize equiv_ins; clear equiv_ins.
(* Goal: forall (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a') (_ : LOOKUP unit i0 a' tt), LOOKUP unit i0 a tt *)
elim a; clear a; intros t avl_t.
(* Goal: forall (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit t avl_t) a') (_ : LOOKUP unit i0 a' tt), LOOKUP unit i0 (AVL_intro unit t avl_t) tt *)
elim a'; clear a'; intros t' avl_t'.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: forall _ : equiv_ins unit i (fun _ : unit => tt) tt t t', lookup unit i t' tt *)
elim (lookup_dec unit i t avl_t).
(* Goal: forall (_ : forall d : unit, not (lookup unit i t d)) (_ : equiv_ins unit i (fun _ : unit => tt) tt t t'), lookup unit i t' tt *)
intros.
(* Goal: AvlTrees.lookup unit i0 t tt *)
inversion_clear equiv_ins.
(* Goal: lookup unit i t' tt *)
(* Goal: forall (_ : forall d : unit, not (lookup unit i t d)) (_ : equiv_ins unit i (fun _ : unit => tt) tt t t'), lookup unit i t' tt *)
apply H with d.
(* Goal: Equal i i *)
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply equal_refl.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
assumption.
(* Goal: forall (_ : forall d : unit, not (lookup unit i t d)) (_ : equiv_ins unit i (fun _ : unit => tt) tt t t'), lookup unit i t' tt *)
intros.
(* Goal: AvlTrees.lookup unit i0 t tt *)
inversion_clear equiv_ins.
(* Goal: lookup unit i t' tt *)
apply H0.
(* Goal: Equal i i *)
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply equal_refl.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
assumption.
Qed.




Lemma in_ngamma_ins_a_rev :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (ai : atomic_imps) (i : Int) (a a' : atoms) (c : normal_form),
 EQUIV_INS unit i (fun _ : unit => tt) tt a a' ->
 in_ngamma work ds ni ai a' c -> in_ngamma work ds ni ai a c + {c = NAtom i}.
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (i : Int) (a a' : atoms) (c : normal_form) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a') (_ : in_ngamma work ds ni ai a' c), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros work ds ni ai i a a' c equiv_ins in_ngamma0.
(* Goal: sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
elim in_ngamma0; clear in_ngamma0 c.
(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n work c), sumor (in_ngamma work ds ni ai a c) (@eq normal_form c (NAtom i)) *)
(* Goal: forall (n : nat) (i0 j : Int) (_ : my_nth disj n ds (@pair Int Int i0 j)), sumor (in_ngamma work ds ni ai a (NDisj i0 j)) (@eq normal_form (NDisj i0 j) (NAtom i)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) (NAtom i)) *)
(* Goal: forall (i0 : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i0 b)) (@eq normal_form (AImp i0 b) (NAtom i)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a' tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intros n c0 nth; left; apply In_Work with n; assumption.
(* Goal: forall (n : nat) (i0 j : Int) (_ : my_nth disj n ds (@pair Int Int i0 j)), sumor (in_ngamma work ds ni ai a (NDisj i0 j)) (@eq normal_form (NDisj i0 j) (NAtom i)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps ni) x), sumor (in_ngamma work ds ni ai a (NImp_NF x)) (@eq normal_form (NImp_NF x) (NAtom i)) *)
(* Goal: forall (i0 : Int) (b : normal_form) (n : nat) (bs : nf_list) (_ : LOOKUP nf_list i0 ai bs) (_ : my_nth normal_form n bs b), sumor (in_ngamma work ds ni ai a (AImp i0 b)) (@eq normal_form (AImp i0 b) (NAtom i)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a' tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intros n i' j' nth; left; apply In_Disjs with n; assumption.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
intros n x' nth; left; apply In_Nested_Imps with n; assumption.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
intros i0 b n bs lookup nth; left; apply In_Atomic_Imps with n bs; assumption.

(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a' tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intros i0 lookup.
(* Goal: sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
elim (equal_dec i0 i).
(* Goal: forall _ : Equal i0 i, sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
(* Goal: forall _ : not (Equal i0 i), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intro equal.
(* Goal: sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
(* Goal: forall _ : not (Equal i0 i), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
right.
(* Goal: @eq normal_form (AImp i b0) (AImp i b0) *)
(* Goal: forall _ : not (Equal i0 i), sum (in_ngamma work ds ni ai a (AImp i0 b0)) (in_ngamma_del_ai_rev_spec i bs (AImp i0 b0)) *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sum (in_ngamma work ds ni ai a (NAtom i0)) (in_ngamma_del_ai_rev_spec i bs (NAtom i0)) *)
 rewrite (equal_eq i0 i); trivial.
(* Goal: forall _ : not (Equal i0 i), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (NAtom i)) *)
intros notequal.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
left; apply In_Atoms.
(* Goal: LOOKUP unit i0 a tt *)
generalize equiv_ins lookup; clear equiv_ins lookup.
(* Goal: forall (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a') (_ : LOOKUP unit i0 a' tt), LOOKUP unit i0 a tt *)
elim a; clear a; intros t avl_t.
(* Goal: forall (_ : EQUIV_INS unit i (fun _ : unit => tt) tt (AVL_intro unit t avl_t) a') (_ : LOOKUP unit i0 a' tt), LOOKUP unit i0 (AVL_intro unit t avl_t) tt *)
elim a'; clear a'; intros t' avl_t'.
(* Goal: forall (_ : equiv_ins nf_list i (@cons normal_form b) nf_nil t t') (_ : lookup nf_list i0 t' bs), lookup nf_list i0 t bs *)
(* Goal: my_nth normal_form n bs b0 *)
(* Goal: forall (i0 : Int) (_ : LOOKUP unit i0 a tt), sumor (in_ngamma work ds ni ai a (NAtom i0)) (@eq normal_form (NAtom i0) (AImp i b)) *)
simpl in |- *; intros equiv_ins lookup.
(* Goal: AvlTrees.lookup unit i0 t tt *)
inversion_clear equiv_ins.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply H2; assumption.
Qed.







(********************************************************************)


Lemma in_ngamma_shift_work_ds :
 forall (i j : Int) (work : nf_list) (ds : disjs) (ni : nested_imps)
   (ai : atomic_imps) (a : atoms) (c : normal_form),
 in_ngamma (NDisj i j :: work) ds ni ai a c ->
 in_ngamma work ((i, j) :: ds) ni ai a c.
(* Goal: forall (i j : Int) (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma work (@cons (prod Int Int) (@pair Int Int i j) ds) ni ai a c), in_ngamma (@cons normal_form (NDisj i j) work) ds ni ai a c *)
intros i j work ds ni ai a c in_ngamma0.
elim (in_ngamma_cons_work_rev (NDisj i j) work ds ni ai a c in_ngamma0);
 clear in_ngamma0.
(* Goal: forall _ : in_ngamma work ds ni ai a c, in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
(* Goal: forall _ : @eq normal_form c (NAtom i), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros in_ngamma0.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_cons_ds_tail; assumption.
intros eq_c;  rewrite eq_c.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: in_ngamma work (@cons (prod Int Int) (@pair Int Int i j) ds) ni ai a (NDisj i j) *)
apply in_ngamma_cons_ds_head.
Qed.


Lemma in_ngamma_shift_ds_work :
 forall (i j : Int) (work : nf_list) (ds : disjs) (ni : nested_imps)
   (ai : atomic_imps) (a : atoms) (c : normal_form),
 in_ngamma work ((i, j) :: ds) ni ai a c ->
 in_ngamma (NDisj i j :: work) ds ni ai a c.
(* Goal: forall (i j : Int) (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma work (@cons (prod Int Int) (@pair Int Int i j) ds) ni ai a c), in_ngamma (@cons normal_form (NDisj i j) work) ds ni ai a c *)
intros i j work ds ni ai a c in_ngamma0.
elim (in_ngamma_cons_ds_rev work i j ds ni ai a c in_ngamma0);
 clear in_ngamma0.
(* Goal: forall _ : in_ngamma work ds ni ai a c, in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
(* Goal: forall _ : @eq normal_form c (NAtom i), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros in_ngamma0.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_cons_work_tail; assumption.
intros eq_c;  rewrite eq_c.
(* Goal: in_ngamma (@cons normal_form (NDisj i j) work) ds ni ai a (NDisj i j) *)
apply in_ngamma_cons_work_head with (c := NDisj i j).
Qed.


Lemma in_ngamma_shift_work_ni :
 forall (x : nested_imp) (work : nf_list) (ds : disjs) 
   (ni : nested_imps) (ai : atomic_imps) (a : atoms) 
   (c : normal_form),
 in_ngamma (NImp_NF (nested_imp2nimp x) :: work) ds ni ai a c ->
 in_ngamma work ds (x :: ni) ai a c.
(* Goal: forall (x : nested_imp) (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma work ds (@cons nested_imp x ni) ai a c), in_ngamma (@cons normal_form (NImp_NF (nested_imp2nimp x)) work) ds ni ai a c *)
intros x work ds ni ai a c in_ngamma0.
elim
 (in_ngamma_cons_work_rev (NImp_NF (nested_imp2nimp x)) work ds ni ai a c
    in_ngamma0); clear in_ngamma0.
(* Goal: forall _ : in_ngamma work ds ni ai a c, in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
(* Goal: forall _ : @eq normal_form c (NAtom i), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros in_ngamma0.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_cons_ni_tail; assumption.
intros eq_c;  rewrite eq_c.
(* Goal: in_ngamma work ds (@cons nested_imp x ni) ai a (NImp_NF (nested_imp2nimp x)) *)
apply in_ngamma_cons_ni_head. 
Qed.


Lemma in_ngamma_shift_ni_work :
 forall (x : nested_imp) (work : nf_list) (ds : disjs) 
   (ni : nested_imps) (ai : atomic_imps) (a : atoms) 
   (c : normal_form),
 in_ngamma work ds (x :: ni) ai a c ->
 in_ngamma (NImp_NF (nested_imp2nimp x) :: work) ds ni ai a c.
(* Goal: forall (x : nested_imp) (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma work ds (@cons nested_imp x ni) ai a c), in_ngamma (@cons normal_form (NImp_NF (nested_imp2nimp x)) work) ds ni ai a c *)
intros x work ds ni ai a c in_ngamma0.
(* Goal: in_ngamma (@cons normal_form (NImp_NF (nested_imp2nimp x)) work) ds ni ai a c *)
elim (in_ngamma_cons_ni_rev work ds x ni ai a c in_ngamma0); clear in_ngamma0.
(* Goal: forall _ : in_ngamma work ds ni ai a c, in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
(* Goal: forall _ : @eq normal_form c (NAtom i), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros in_ngamma0.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_cons_work_tail; assumption.
intros eq_c;  rewrite eq_c.
(* Goal: in_ngamma (@cons normal_form (AImp i b) work) ds ni ai a (AImp i b) *)
apply in_ngamma_cons_work_head. 
Qed.


Lemma in_ngamma_shift_work_ni_x_ni :
 forall (x : nested_imp) (work : nf_list) (ds : disjs)
   (ni1 ni2 : nested_imps) (ai : atomic_imps) (a : atoms) 
   (c : normal_form),
 in_ngamma (NImp_NF (nested_imp2nimp x) :: work) ds (ni1 ++ ni2) ai a c ->
 in_ngamma work ds (ni1 ++ x :: ni2) ai a c.
(* Goal: forall (x : nested_imp) (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a c), in_ngamma (@cons normal_form (NImp_NF (nested_imp2nimp x)) work) ds (@app nested_imp ni1 ni2) ai a c *)
intros x work ds ni1 ni2 ai a c in_ngamma0.
elim
 (in_ngamma_cons_work_rev (NImp_NF (nested_imp2nimp x)) work ds 
    (ni1 ++ ni2) ai a c in_ngamma0); clear in_ngamma0.
(* Goal: forall _ : in_ngamma work ds ni ai a c, in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
(* Goal: forall _ : @eq normal_form c (NAtom i), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros in_ngamma0.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_ni_x_ni_tail; assumption.
intros eq_c;  rewrite eq_c.
(* Goal: in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a (NImp_NF (nested_imp2nimp x)) *)
apply in_ngamma_ni_x_ni_head with (x := x).
Qed.


Lemma in_ngamma_shift_ni_x_ni_work :
 forall (x : nested_imp) (work : nf_list) (ds : disjs)
   (ni1 ni2 : nested_imps) (ai : atomic_imps) (a : atoms) 
   (c : normal_form),
 in_ngamma work ds (ni1 ++ x :: ni2) ai a c ->
 in_ngamma (NImp_NF (nested_imp2nimp x) :: work) ds (ni1 ++ ni2) ai a c.
(* Goal: forall (x : nested_imp) (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : in_ngamma work ds (@app nested_imp ni1 (@cons nested_imp x ni2)) ai a c), in_ngamma (@cons normal_form (NImp_NF (nested_imp2nimp x)) work) ds (@app nested_imp ni1 ni2) ai a c *)
intros x work ds ni1 ni2 ai a c in_ngamma0.
elim (in_ngamma_ni_x_ni_rev work ds x ni1 ni2 ai a c in_ngamma0);
 clear in_ngamma0.
(* Goal: forall _ : in_ngamma work ds ni ai a c, in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
(* Goal: forall _ : @eq normal_form c (NAtom i), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros in_ngamma0.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_cons_work_tail; assumption.
intros eq_c;  rewrite eq_c.
(* Goal: in_ngamma (@cons normal_form (AImp i b) work) ds ni ai a (AImp i b) *)
apply in_ngamma_cons_work_head. 
Qed.



Lemma in_ngamma_shift_work_ai_new :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (i : Int) (b : normal_form) (ai ai' : atomic_imps) 
   (a : atoms) (c : normal_form),
 (forall bs : nf_list, LOOKUP nf_list i ai bs -> False) ->
 EQUIV_INS nf_list i (cons b) nf_nil ai ai' ->
 in_ngamma (AImp i b :: work) ds ni ai a c -> in_ngamma work ds ni ai' a c.
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (i : Int) (b : normal_form) (ai ai' : atomic_imps) (a : atoms) (c : normal_form) (_ : forall (bs : nf_list) (_ : LOOKUP nf_list i ai bs), False) (_ : EQUIV_INS nf_list i (@cons normal_form b) nf_nil ai ai') (_ : in_ngamma (@cons normal_form (AImp i b) work) ds ni ai a c), in_ngamma work ds ni ai' a c *)
intros work ds ni i b ai ai' a c notlookup equiv_ins in_ngamma0.
elim (in_ngamma_cons_work_rev (AImp i b) work ds ni ai a c in_ngamma0);
 clear in_ngamma0.
(* Goal: forall _ : in_ngamma work ds ni ai a c, in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
(* Goal: forall _ : @eq normal_form c (NAtom i), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros in_ngamma0.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_ins_ai_tail with i b ai; assumption.
intros eq_c;  rewrite eq_c.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_ins_ai_head_new with ai; assumption.
Qed.


Lemma in_ngamma_shift_work_ai_old :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (i : Int) (b : normal_form) (bs : nf_list) (ai ai' : atomic_imps)
   (a : atoms) (c : normal_form),
 LOOKUP nf_list i ai bs ->
 EQUIV_INS nf_list i (cons b) nf_nil ai ai' ->
 in_ngamma (AImp i b :: work) ds ni ai a c -> in_ngamma work ds ni ai' a c.
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (i : Int) (b : normal_form) (bs : nf_list) (ai ai' : atomic_imps) (a : atoms) (c : normal_form) (_ : LOOKUP nf_list i ai bs) (_ : EQUIV_INS nf_list i (@cons normal_form b) nf_nil ai ai') (_ : in_ngamma (@cons normal_form (AImp i b) work) ds ni ai a c), in_ngamma work ds ni ai' a c *)
intros work ds ni i b bs ai ai' a c lookup equiv_ins in_ngamma0.
elim (in_ngamma_cons_work_rev (AImp i b) work ds ni ai a c in_ngamma0);
 clear in_ngamma0.
(* Goal: forall _ : in_ngamma work ds ni ai a c, in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
(* Goal: forall _ : @eq normal_form c (NAtom i), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros in_ngamma0.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_ins_ai_tail with i b ai; assumption.
intros eq_c;  rewrite eq_c.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_ins_ai_head_old with bs ai; assumption.
Qed.


Lemma in_ngamma_shift_ai_work :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (i : Int) (b : normal_form) (ai ai' : atomic_imps) 
   (a : atoms) (c : normal_form),
 EQUIV_INS nf_list i (cons b) nf_nil ai ai' ->
 in_ngamma work ds ni ai' a c -> in_ngamma (AImp i b :: work) ds ni ai a c.
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (i : Int) (b : normal_form) (ai ai' : atomic_imps) (a : atoms) (c : normal_form) (_ : EQUIV_INS nf_list i (@cons normal_form b) nf_nil ai ai') (_ : in_ngamma work ds ni ai' a c), in_ngamma (@cons normal_form (AImp i b) work) ds ni ai a c *)
intros work ds ni i b ai ai' a c equiv_ins in_ngamma0.
elim (in_ngamma_ins_ai_rev work ds ni i b ai ai' a c); try assumption;
 clear in_ngamma0.
(* Goal: forall _ : in_ngamma work ds ni ai a c, in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
(* Goal: forall _ : @eq normal_form c (NAtom i), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros in_ngamma0.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_cons_work_tail; assumption.
intros eq_c;  rewrite eq_c.
(* Goal: in_ngamma (@cons normal_form (AImp i b) work) ds ni ai a (AImp i b) *)
apply in_ngamma_cons_work_head.
Qed.


Lemma in_ngamma_shift_work_a :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (ai : atomic_imps) (i : Int) (a a' : atoms) (c : normal_form),
 EQUIV_INS unit i (fun _ : unit => tt) tt a a' ->
 in_ngamma (NAtom i :: work) ds ni ai a c -> in_ngamma work ds ni ai a' c.
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (i : Int) (a a' : atoms) (c : normal_form) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a') (_ : in_ngamma work ds ni ai a' c), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros work ds ni ai i a a' c equiv_ins in_ngamma0.
elim (in_ngamma_cons_work_rev (NAtom i) work ds ni ai a c in_ngamma0);
 clear in_ngamma0.
(* Goal: forall _ : in_ngamma work ds ni ai a c, in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
(* Goal: forall _ : @eq normal_form c (NAtom i), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros in_ngamma0.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_ins_a_tail with i a; assumption.
intros eq_c;  rewrite eq_c.
(* Goal: in_ngamma work ds ni ai a' (NAtom i) *)
simpl in |- *.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_ins_a_head with a; assumption.
Qed.


Lemma in_ngamma_shift_a_work :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (ai : atomic_imps) (i : Int) (a a' : atoms) (c : normal_form),
 EQUIV_INS unit i (fun _ : unit => tt) tt a a' ->
 in_ngamma work ds ni ai a' c -> in_ngamma (NAtom i :: work) ds ni ai a c.
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (i : Int) (a a' : atoms) (c : normal_form) (_ : EQUIV_INS unit i (fun _ : unit => tt) tt a a') (_ : in_ngamma work ds ni ai a' c), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros work ds ni ai i a a' c equiv_ins in_ngamma0.
elim (in_ngamma_ins_a_rev work ds ni ai i a a' c); try assumption;
 clear in_ngamma0.
(* Goal: forall _ : in_ngamma work ds ni ai a c, in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
(* Goal: forall _ : @eq normal_form c (NAtom i), in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a c *)
intros in_ngamma0.
(* Goal: forall (data : unit) (_ : lookup unit i t data), False *)
apply in_ngamma_cons_work_tail; assumption.
intros eq_c;  rewrite eq_c.
(* Goal: in_ngamma (@cons normal_form (NAtom i) work) ds ni ai a (NAtom i) *)
apply in_ngamma_cons_work_head with (c := NAtom i).
Qed.

