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

Require Export Disjunct.
Require Export NDeco_Sound.


Fixpoint n2forest (n : nested_imps) : Forest atoms :=
  match n with
  | nil => Nil_Forest atoms
  | Undecorated _ :: n => n2forest n
  | Decorated _ k :: n => Cons_Forest atoms k (n2forest n)
  end.


Remark cons_counter_model_suc :
 forall (x : nimp) (k : kripke_tree) (ni : nested_imps) (a : atoms),
 In (Decorated x k) ni -> Suc k (node atoms a (n2forest ni)).
(* Goal: forall (x : nimp) (k : kripke_tree) (ni : nested_imps) (a : atoms) (_ : @In nested_imp (Decorated x k) ni), Suc k (node atoms a (n2forest ni)) *)
intros x k ni a in_k.
(* Goal: Suc k (node atoms a (n2forest ni)) *)
unfold Suc in |- *; apply successor_trans with k.
(* Goal: In_Forest atoms k (successors atoms (node atoms a (n2forest ni))) *)
(* Goal: Successor atoms k k *)
generalize in_k; clear in_k.
(* Goal: forall (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) ni), False) (_ : deco_sound nf_nil DNil ni ai a), Is_Monotone_kripke_tree (node atoms a (n2forest ni)) *)
elim ni; clear ni. 
(* Goal: forall _ : In_Forest atoms k (n2forest (@nil nested_imp)), @ex nimp (fun x : nimp => @In nested_imp (Decorated x k) (@nil nested_imp)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall _ : In_Forest atoms k (n2forest l), @ex nimp (fun x : nimp => @In nested_imp (Decorated x k) l)) (_ : In_Forest atoms k (n2forest (@cons nested_imp a l))), @ex nimp (fun x : nimp => @In nested_imp (Decorated x k) (@cons nested_imp a l)) *)
intros in_k.
(* Goal: @ex nimp (fun x0 : nimp => or (@eq nested_imp (Decorated x k0) (Decorated x0 k)) (@In nested_imp (Decorated x0 k) ni)) *)
inversion_clear in_k.
(* Goal: forall (a0 : nested_imp) (l : list nested_imp) (_ : forall _ : @In nested_imp (Decorated x k) l, In_Forest atoms k (successors atoms (node atoms a (n2forest l)))) (_ : @In nested_imp (Decorated x k) (@cons nested_imp a0 l)), In_Forest atoms k (successors atoms (node atoms a (n2forest (@cons nested_imp a0 l)))) *)
(* Goal: Successor atoms k k *)
intros y ni ih in_k.
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni))) *)
unfold n2forest in |- *; simpl in |- *; fold n2forest in |- *.
(* Goal: @ex nimp (fun x0 : nimp => or (@eq nested_imp (Decorated x k0) (Decorated x0 k)) (@In nested_imp (Decorated x0 k) ni)) *)
inversion_clear in_k.
(* Goal: In_Forest atoms k match y with | Undecorated n0 => n2forest ni | Decorated n0 k => Cons_Forest atoms k (n2forest ni) end *)
(* Goal: In_Forest atoms k match y with | Undecorated n0 => n2forest ni | Decorated n0 k => Cons_Forest atoms k (n2forest ni) end *)
(* Goal: Successor atoms k k *)
 rewrite H; clear H y.
(* Goal: In_Forest atoms k (Cons_Forest atoms k (n2forest ni)) *)
(* Goal: In_Forest atoms k match y with | Undecorated n0 => n2forest ni | Decorated n0 k => Cons_Forest atoms k (n2forest ni) end *)
(* Goal: Successor atoms k k *)
apply in_forest_head.
(* Goal: In_Forest atoms k match y with | Undecorated n0 => n2forest ni | Decorated n0 k => Cons_Forest atoms k (n2forest ni) end *)
(* Goal: Successor atoms k k *)
generalize (ih H); clear ih H.
(* Goal: forall _ : In_Forest atoms k (successors atoms (node atoms a (n2forest ni))), In_Forest atoms k match y with | Undecorated n0 => n2forest ni | Decorated n0 k => Cons_Forest atoms k (n2forest ni) end *)
(* Goal: Successor atoms k k *)
intros ih.
(* Goal: In_Forest atoms k match y with | Undecorated n0 => n2forest ni | Decorated n0 k => Cons_Forest atoms k (n2forest ni) end *)
(* Goal: Successor atoms k k *)
case y; clear y.
(* Goal: forall _ : False, False *)
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall _ : @In nested_imp (Undecorated x) (rev_app l NNil), False) (_ : @In nested_imp (Undecorated x) (rev_app (@cons decorated_nested_imp a l) NNil)), False *)
intros; assumption.
(* Goal: forall (_ : nimp) (k0 : kripke_tree), In_Forest atoms k (Cons_Forest atoms k0 (n2forest ni)) *)
(* Goal: Successor atoms k k *)
intros; apply in_forest_tail; assumption.
(* Goal: Successor atoms k k *)
apply successor_refl.
Qed.



Remark in_forest_ex_a0a1b :
 forall (k : kripke_tree) (ni : nested_imps),
 In_Forest atoms k (n2forest ni) -> exists x : nimp, In (Decorated x k) ni.
(* Goal: forall (k : kripke_tree) (ni : nested_imps) (_ : In_Forest atoms k (n2forest ni)), @ex nimp (fun x : nimp => @In nested_imp (Decorated x k) ni) *)
intros k ni.
(* Goal: forall (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) ni), False) (_ : deco_sound nf_nil DNil ni ai a), Is_Monotone_kripke_tree (node atoms a (n2forest ni)) *)
elim ni; clear ni.
(* Goal: forall _ : In_Forest atoms k (n2forest (@nil nested_imp)), @ex nimp (fun x : nimp => @In nested_imp (Decorated x k) (@nil nested_imp)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall _ : In_Forest atoms k (n2forest l), @ex nimp (fun x : nimp => @In nested_imp (Decorated x k) l)) (_ : In_Forest atoms k (n2forest (@cons nested_imp a l))), @ex nimp (fun x : nimp => @In nested_imp (Decorated x k) (@cons nested_imp a l)) *)
intros in_k.
(* Goal: @ex nimp (fun x0 : nimp => or (@eq nested_imp (Decorated x k0) (Decorated x0 k)) (@In nested_imp (Decorated x0 k) ni)) *)
inversion_clear in_k.
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni))) *)
unfold n2forest in |- *; simpl in |- *; fold n2forest in |- *.
(* Goal: forall (x : nested_imp) (_ : and (my_nth nested_imp n (rev_app dni NNil) x) (@eq nimp (nested_imp2nimp x) (NImp a0 a1 b))), False *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros x; case x; clear x.
(* Goal: forall (n : nimp) (l : list nested_imp) (_ : forall _ : In_Forest atoms k (n2forest l), @ex nimp (fun x : nimp => @In nested_imp (Decorated x k) l)) (_ : In_Forest atoms k (n2forest l)), @ex nimp (fun x : nimp => or (@eq nested_imp (Undecorated n) (Decorated x k)) (@In nested_imp (Decorated x k) l)) *)
(* Goal: forall (n : nimp) (k0 : kripke_tree) (l : list nested_imp) (_ : forall _ : In_Forest atoms k (n2forest l), @ex nimp (fun x : nimp => @In nested_imp (Decorated x k) l)) (_ : In_Forest atoms k (Cons_Forest atoms k0 (n2forest l))), @ex nimp (fun x : nimp => or (@eq nested_imp (Decorated n k0) (Decorated x k)) (@In nested_imp (Decorated x k) l)) *)
intros x ni ih in_k.
(* Goal: @ex nimp (fun x0 : nimp => or (@eq nested_imp (Undecorated x) (Decorated x0 k)) (@In nested_imp (Decorated x0 k) ni)) *)
(* Goal: forall (n : nimp) (k0 : kripke_tree) (l : list nested_imp) (_ : forall _ : In_Forest atoms k (n2forest l), @ex nimp (fun x : nimp => @In nested_imp (Decorated x k) l)) (_ : In_Forest atoms k (Cons_Forest atoms k0 (n2forest l))), @ex nimp (fun x : nimp => or (@eq nested_imp (Decorated n k0) (Decorated x k)) (@In nested_imp (Decorated x k) l)) *)
elim ih; clear ih.
(* Goal: forall (x0 : nimp) (_ : @In nested_imp (Decorated x0 k) ni), @ex nimp (fun x1 : nimp => or (@eq nested_imp (Undecorated x) (Decorated x1 k)) (@In nested_imp (Decorated x1 k) ni)) *)
(* Goal: In_Forest atoms k (n2forest ni) *)
(* Goal: forall (n : nimp) (k0 : kripke_tree) (l : list nested_imp) (_ : forall _ : In_Forest atoms k (n2forest l), @ex nimp (fun x : nimp => @In nested_imp (Decorated x k) l)) (_ : In_Forest atoms k (Cons_Forest atoms k0 (n2forest l))), @ex nimp (fun x : nimp => or (@eq nested_imp (Decorated n k0) (Decorated x k)) (@In nested_imp (Decorated x k) l)) *)
intros y in_y.
(* Goal: @sig nested_imp (fun y0 : nested_imp => and (my_nth nested_imp O (@cons nested_imp y ni) y0) (@eq nimp (nested_imp2nimp y0) x)) *)
(* Goal: forall (n : nat) (_ : forall (ni : nested_imps) (_ : my_nth nimp n (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp n ni y) (@eq nimp (nested_imp2nimp y) x))) (ni : nested_imps) (_ : my_nth nimp (S n) (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) ni y) (@eq nimp (nested_imp2nimp y) x)) *)
exists y.
(* Goal: @In nested_imp (Undecorated x) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
(* Goal: deco_sound nf_nil DNil ni ai a *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
right; assumption.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: forall (n : nimp) (k0 : kripke_tree) (l : list nested_imp) (_ : forall _ : In_Forest atoms k (n2forest l), @ex nimp (fun x : nimp => @In nested_imp (Decorated x k) l)) (_ : In_Forest atoms k (Cons_Forest atoms k0 (n2forest l))), @ex nimp (fun x : nimp => or (@eq nested_imp (Decorated n k0) (Decorated x k)) (@In nested_imp (Decorated x k) l)) *)
intros x k0 ni ih in_k.
(* Goal: @ex nimp (fun x0 : nimp => or (@eq nested_imp (Decorated x k0) (Decorated x0 k)) (@In nested_imp (Decorated x0 k) ni)) *)
inversion_clear in_k.
(* Goal: @ex nimp (fun x0 : nimp => or (@eq nested_imp (Decorated x k0) (Decorated x0 k0)) (@In nested_imp (Decorated x0 k0) ni)) *)
(* Goal: @ex nimp (fun x0 : nimp => or (@eq nested_imp (Decorated x k0) (Decorated x0 k)) (@In nested_imp (Decorated x0 k) ni)) *)
exists x.
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
left; trivial.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
elim ih; try assumption.
(* Goal: forall (x0 : nimp) (_ : @In nested_imp (Decorated x0 k) ni), @ex nimp (fun x1 : nimp => or (@eq nested_imp (Decorated x k0) (Decorated x1 k)) (@In nested_imp (Decorated x1 k) ni)) *)
intros x0 in_k.
(* Goal: @ex nimp (fun x0 : nimp => or (@eq nested_imp (Decorated x k0) (Decorated x0 k)) (@In nested_imp (Decorated x0 k) ni)) *)
exists x0.
(* Goal: @In nested_imp (Undecorated x) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
(* Goal: deco_sound nf_nil DNil ni ai a *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
right; assumption.
Qed.

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


Remark deco_sound_in_forest_forces :
 forall (work : nf_list) (ds : disjs) (ni : nested_imps) 
   (ai : atomic_imps) (a : atoms) (k : kripke_tree) 
   (c : normal_form),
 deco_sound work ds ni ai a ->
 In_Forest atoms k (n2forest ni) ->
 in_ngamma work ds ni ai a c -> forces_t k (nf2form c).
(* Goal: forall (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps) (a : atoms) (k : kripke_tree) (c : normal_form) (_ : deco_sound work ds ni ai a) (_ : In_Forest atoms k (n2forest ni)) (_ : in_ngamma work ds ni ai a c), forces_t k (nf2form c) *)
intros work ds ni ai a k c complete in_k in_ngamma.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
elim in_forest_ex_a0a1b with k ni; try assumption.
(* Goal: forall (x : nested_imp) (_ : and (my_nth nested_imp n (rev_app dni NNil) x) (@eq nimp (nested_imp2nimp x) (NImp a0 a1 b))), False *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros x; case x; clear x. 
(* Goal: forall (i i0 : Int) (n : normal_form) (_ : @In nested_imp (Decorated (NImp i i0 n) k) ni), forces_t k (nf2form c) *)
intros a0 a1 b in_x.
(* Goal: forces_t k (nf2form c) *)
elim (complete k a0 a1 b in_x); clear complete.
(* Goal: forall (_ : Is_Monotone_kripke_tree k) (_ : forces_ngamma nf_nil DNil (rev_app dni NNil) ai a k) (_ : forall _ : forces_t k (Imp (Atom a0) (Atom a1)), False), False *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (rev_app dni NNil) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros k_is_mon k_forces_ngamma k_notforces_a0a1.
(* Goal: forces_t k (nf2form c) *)
apply k_forces_ngamma.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
Qed.

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

Remark cons_counter_model_mon :
 forall (ni : nested_imps) (ai : atomic_imps) (a : atoms),
 (forall x : nimp, In (Undecorated x) ni -> False) ->
 deco_sound nf_nil DNil ni ai a ->
 Is_Monotone_kripke_tree (node atoms a (n2forest ni)).
(* Goal: forall (ni : nested_imps) (ai : atomic_imps) (a : atoms) (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) ni), False) (_ : deco_sound nf_nil DNil ni ai a), Is_Monotone_kripke_tree (node atoms a (n2forest ni)) *)
intros ni ai a.
(* Goal: forall (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) ni), False) (_ : deco_sound nf_nil DNil ni ai a), Is_Monotone_kripke_tree (node atoms a (n2forest ni)) *)
elim ni; clear ni.
(* Goal: forall (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) (@nil nested_imp)), False) (_ : deco_sound nf_nil DNil (@nil nested_imp) ai a), Is_Monotone_kripke_tree (node atoms a (n2forest (@nil nested_imp))) *)
(* Goal: forall (a0 : nested_imp) (l : list nested_imp) (_ : forall (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) l), False) (_ : deco_sound nf_nil DNil l ai a), Is_Monotone_kripke_tree (node atoms a (n2forest l))) (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) (@cons nested_imp a0 l)), False) (_ : deco_sound nf_nil DNil (@cons nested_imp a0 l) ai a), Is_Monotone_kripke_tree (node atoms a (n2forest (@cons nested_imp a0 l))) *)
intros all_ref complete.
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (@nil nested_imp))) *)
(* Goal: forall (a0 : nested_imp) (l : list nested_imp) (_ : forall (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) l), False) (_ : deco_sound nf_nil DNil l ai a), Is_Monotone_kripke_tree (node atoms a (n2forest l))) (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) (@cons nested_imp a0 l)), False) (_ : deco_sound nf_nil DNil (@cons nested_imp a0 l) ai a), Is_Monotone_kripke_tree (node atoms a (n2forest (@cons nested_imp a0 l))) *)
unfold n2forest in |- *.
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Atom j) (nf2form b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
simpl in |- *.
(* Goal: Is_Monotone_kripke_tree (node atoms a (Cons_Forest atoms k (n2forest ni))) *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
unfold Is_Monotone_kripke_tree in |- *.
(* Goal: Is_Monotone_Tree atoms Int forces0_t (node atoms a (Cons_Forest atoms k (n2forest ni))) *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
apply is_monotone_tree_intro.
(* Goal: Is_Monotone_Forest atoms Int forces0_t a (Nil_Forest atoms) *)
(* Goal: forall (a0 : nested_imp) (l : list nested_imp) (_ : forall (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) l), False) (_ : deco_sound nf_nil DNil l ai a), Is_Monotone_kripke_tree (node atoms a (n2forest l))) (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) (@cons nested_imp a0 l)), False) (_ : deco_sound nf_nil DNil (@cons nested_imp a0 l) ai a), Is_Monotone_kripke_tree (node atoms a (n2forest (@cons nested_imp a0 l))) *)
apply is_monotone_forest_nil.

(* Goal: forall (ni : nested_imps) (_ : my_nth nimp O (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp O ni y) (@eq nimp (nested_imp2nimp y) x)) *)
(* Goal: forall (n : nat) (_ : forall (ni : nested_imps) (_ : my_nth nimp n (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp n ni y) (@eq nimp (nested_imp2nimp y) x))) (ni : nested_imps) (_ : my_nth nimp (S n) (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) ni y) (@eq nimp (nested_imp2nimp y) x)) *)
intros ni; case ni; clear ni.
(* Goal: forall (n : nimp) (l : list nested_imp) (_ : forall (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) l), False) (_ : deco_sound nf_nil DNil l ai a), Is_Monotone_kripke_tree (node atoms a (n2forest l))) (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) (@cons nested_imp (Undecorated n) l)), False) (_ : deco_sound nf_nil DNil (@cons nested_imp (Undecorated n) l) ai a), Is_Monotone_kripke_tree (node atoms a (n2forest (@cons nested_imp (Undecorated n) l))) *)
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) l), False) (_ : deco_sound nf_nil DNil l ai a), Is_Monotone_kripke_tree (node atoms a (n2forest l))) (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) (@cons nested_imp (Decorated n k) l)), False) (_ : deco_sound nf_nil DNil (@cons nested_imp (Decorated n k) l) ai a), Is_Monotone_kripke_tree (node atoms a (n2forest (@cons nested_imp (Decorated n k) l))) *)
intros x ni ih all_ref complete.
(* Goal: forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form b) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Atom j) (nf2form b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
elimtype False.
(* Goal: False *)
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) l), False) (_ : deco_sound nf_nil DNil l ai a), Is_Monotone_kripke_tree (node atoms a (n2forest l))) (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) (@cons nested_imp (Decorated n k) l)), False) (_ : deco_sound nf_nil DNil (@cons nested_imp (Decorated n k) l) ai a), Is_Monotone_kripke_tree (node atoms a (n2forest (@cons nested_imp (Decorated n k) l))) *)
apply (all_ref x).
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
left; trivial.
(* Goal: forall (x : nested_imp) (_ : and (my_nth nested_imp n (rev_app dni NNil) x) (@eq nimp (nested_imp2nimp x) (NImp a0 a1 b))), False *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros x; case x; clear x.
(* Goal: forall (i i0 : Int) (n : normal_form) (k : kripke_tree) (l : list nested_imp) (_ : forall (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) l), False) (_ : deco_sound nf_nil DNil l ai a), Is_Monotone_kripke_tree (node atoms a (n2forest l))) (_ : forall (x : nimp) (_ : @In nested_imp (Undecorated x) (@cons nested_imp (Decorated (NImp i i0 n) k) l)), False) (_ : deco_sound nf_nil DNil (@cons nested_imp (Decorated (NImp i i0 n) k) l) ai a), Is_Monotone_kripke_tree (node atoms a (n2forest (@cons nested_imp (Decorated (NImp i i0 n) k) l))) *)
intros a0 a1 b k ni ih all_ref complete.
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni))) *)
unfold n2forest in |- *; simpl in |- *; fold n2forest in |- *.
(* Goal: False *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
elim (complete k a0 a1 b).
(* Goal: forall (_ : Is_Monotone_kripke_tree k) (_ : forces_ngamma nf_nil DNil (rev_app dni NNil) ai a k) (_ : forall _ : forces_t k (Imp (Atom a0) (Atom a1)), False), False *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (rev_app dni NNil) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros k_is_mon k_forces_ngamma k_notforces_a0a1.
(* Goal: Is_Monotone_kripke_tree (node atoms a (Cons_Forest atoms k (n2forest ni))) *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
unfold Is_Monotone_kripke_tree in |- *.
(* Goal: Is_Monotone_Tree atoms Int forces0_t (node atoms a (Cons_Forest atoms k (n2forest ni))) *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
apply is_monotone_tree_intro.
(* Goal: Is_Monotone_Forest atoms Int forces0_t a (Cons_Forest atoms k (n2forest ni)) *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
apply is_monotone_forest_cons.
(* Goal: forall (i : Int) (_ : forces0_t a i), forces0_t (root atoms k) i *)
(* Goal: Is_Monotone_Tree atoms Int forces0_t k *)
(* Goal: Is_Monotone_Forest atoms Int forces0_t a (n2forest ni) *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
intros i forces_i.
(* Goal: forces0_t (root atoms k) i *)
(* Goal: Is_Monotone_Tree atoms Int forces0_t k *)
(* Goal: Is_Monotone_Forest atoms Int forces0_t a (n2forest ni) *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
change (forces_t k (Atom i)) in |- *.
(* Goal: forces_t k (Atom i) *)
(* Goal: Is_Monotone_Tree atoms Int forces0_t k *)
(* Goal: Is_Monotone_Forest atoms Int forces0_t a (n2forest ni) *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
apply k_forces_ngamma with (c := NAtom i).
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply In_Atoms; assumption.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: Is_Monotone_Forest atoms Int forces0_t a (n2forest ni) *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
cut (Is_Monotone_kripke_tree (node atoms a (n2forest ni))).
(* Goal: forall _ : or (@In nested_imp (Undecorated x) (rev_app dni NNil)) (@In nested_imp (Undecorated x) (@cons nested_imp (Decorated y k) NNil)), or (@In nested_imp (Undecorated x) (rev_app dni NNil)) (@In nested_imp (Undecorated x) NNil) *)
(* Goal: or (@In nested_imp (Undecorated x) (rev_app dni NNil)) (@In nested_imp (Undecorated x) (@cons nested_imp (Decorated y k) NNil)) *)
intros claim.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
inversion_clear claim; assumption.
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest ni)) *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
apply ih; clear ih.
(* Goal: forall (x : nimp) (_ : @In nested_imp (Undecorated x) (rev_app dni NNil)), False *)
intros x in_x.
(* Goal: False *)
(* Goal: deco_sound nf_nil DNil ni ai a *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
apply all_ref with x.
(* Goal: @In nested_imp (Undecorated x) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
(* Goal: deco_sound nf_nil DNil ni ai a *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
right; assumption.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply deco_sound_cons_ni_tail with (Decorated (NImp a0 a1 b) k); assumption.
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (@cons nested_imp (Decorated (NImp a0 a1 b) k) ni) *)
left; trivial.
Qed.


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

Inductive Cons_Counter_Model_Spec (goal : Int) (ni : nested_imps)
(ai : atomic_imps) (a : atoms) : Set :=
    cons_counter_model_intro :
      forall k : kripke_tree,
      Is_Monotone_kripke_tree k ->
      forces_ngamma nf_nil DNil ni ai a k ->
      (forces_t k (Atom goal) -> False) ->
      Cons_Counter_Model_Spec goal ni ai a.



Remark all_ref_rev_app_nil :
 forall (dni : decorated_nested_imps) (x : nimp),
 In (Undecorated x) (rev_app dni NNil) -> False.
(* Goal: forall (dni : decorated_nested_imps) (x : nimp) (_ : @In nested_imp (Undecorated x) (rev_app dni NNil)), False *)
intros dni x.
(* Goal: forall _ : @In nested_imp (Undecorated x) (rev_app dni NNil), False *)
elim dni; clear dni.
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Atom j) (nf2form b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
simpl in |- *.
(* Goal: forall _ : False, False *)
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall _ : @In nested_imp (Undecorated x) (rev_app l NNil), False) (_ : @In nested_imp (Undecorated x) (rev_app (@cons decorated_nested_imp a l) NNil)), False *)
intros; assumption.
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall _ : @In nested_imp (Undecorated x) (rev_app l NNil), False) (_ : @In nested_imp (Undecorated x) (rev_app (@cons decorated_nested_imp a l) NNil)), False *)
intros a; case a; clear a.
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list decorated_nested_imp) (_ : forall _ : @In nested_imp (Undecorated x) (rev_app l NNil), False) (_ : @In nested_imp (Undecorated x) (rev_app (@cons decorated_nested_imp (@pair nimp kripke_tree n k) l) NNil)), False *)
intros y k dni ih.
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Atom j) (nf2form b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
simpl in |- *.
(* Goal: forall _ : @In nested_imp (Undecorated x) (rev_app dni (@cons nested_imp (Decorated y k) NNil)), False *)
 rewrite (rev_app_app dni (Decorated y k :: NNil)).
(* Goal: forall _ : @In nested_imp (Undecorated x) (@app nested_imp (rev_app dni NNil) (@cons nested_imp (Decorated y k) NNil)), False *)
intros in_x.
(* Goal: False *)
apply ih.
(* Goal: @In nested_imp (Undecorated x) (rev_app dni NNil) *)
 rewrite (rev_app_app dni NNil).
(* Goal: @In nested_imp (Undecorated x) (@app nested_imp (rev_app dni NNil) NNil) *)
apply in_or_app.
cut
 (In (Undecorated x) (rev_app dni NNil) \/
  In (Undecorated x) (Decorated y k :: NNil)).
(* Goal: forall _ : or (@In nested_imp (Undecorated x) (rev_app dni NNil)) (@In nested_imp (Undecorated x) (@cons nested_imp (Decorated y k) NNil)), or (@In nested_imp (Undecorated x) (rev_app dni NNil)) (@In nested_imp (Undecorated x) NNil) *)
(* Goal: or (@In nested_imp (Undecorated x) (rev_app dni NNil)) (@In nested_imp (Undecorated x) (@cons nested_imp (Decorated y k) NNil)) *)
intros claim.
(* Goal: or (@In nested_imp (Undecorated x) (rev_app dni NNil)) (@In nested_imp (Undecorated x) NNil) *)
(* Goal: or (@In nested_imp (Undecorated x) (rev_app dni NNil)) (@In nested_imp (Undecorated x) (@cons nested_imp (Decorated y k) NNil)) *)
elim claim; clear claim; intro claim.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
left; assumption.
(* Goal: or (@In nested_imp (Undecorated x) (rev_app dni NNil)) (@In nested_imp (Undecorated x) NNil) *)
(* Goal: or (@In nested_imp (Undecorated x) (rev_app dni NNil)) (@In nested_imp (Undecorated x) (@cons nested_imp (Decorated y k) NNil)) *)
right; inversion_clear claim.
(* Goal: @In nested_imp (Undecorated x) NNil *)
(* Goal: @In nested_imp (Undecorated x) NNil *)
(* Goal: or (@In nested_imp (Undecorated x) (rev_app dni NNil)) (@In nested_imp (Undecorated x) (@cons nested_imp (Decorated y k) NNil)) *)
 discriminate H.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: or (@In nested_imp (Undecorated x) (rev_app dni NNil)) (@In nested_imp (Undecorated x) (@cons nested_imp (Decorated y k) NNil)) *)
apply in_app_or.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
Qed.



Remark nth_nimp__nth_nested_imp :
 forall (x : nimp) (n : nat) (ni : nested_imps),
 my_nth nimp n (nested_imps2nimps ni) x ->
 {y : nested_imp | my_nth nested_imp n ni y /\ nested_imp2nimp y = x}.
(* Goal: forall (x : nimp) (n : nat) (ni : nested_imps) (_ : my_nth nimp n (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp n ni y) (@eq nimp (nested_imp2nimp y) x)) *)
intros x n.
(* Goal: forall (ni : nested_imps) (_ : my_nth nimp n (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp n ni y) (@eq nimp (nested_imp2nimp y) x)) *)
elim n; clear n.
(* Goal: forall (ni : nested_imps) (_ : my_nth nimp O (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp O ni y) (@eq nimp (nested_imp2nimp y) x)) *)
(* Goal: forall (n : nat) (_ : forall (ni : nested_imps) (_ : my_nth nimp n (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp n ni y) (@eq nimp (nested_imp2nimp y) x))) (ni : nested_imps) (_ : my_nth nimp (S n) (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) ni y) (@eq nimp (nested_imp2nimp y) x)) *)
intros ni; case ni; clear ni.
(* Goal: forall _ : my_nth nimp (S n) (nested_imps2nimps (@nil nested_imp)) x, @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) (@nil nested_imp) y) (@eq nimp (nested_imp2nimp y) x)) *)
(* Goal: forall (n0 : nested_imp) (l : list nested_imp) (_ : my_nth nimp (S n) (nested_imps2nimps (@cons nested_imp n0 l)) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) (@cons nested_imp n0 l) y) (@eq nimp (nested_imp2nimp y) x)) *)
intros nth; elimtype False; inversion_clear nth.
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : my_nth nimp O (nested_imps2nimps (@cons nested_imp n l)) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp O (@cons nested_imp n l) y) (@eq nimp (nested_imp2nimp y) x)) *)
(* Goal: forall (n : nat) (_ : forall (ni : nested_imps) (_ : my_nth nimp n (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp n ni y) (@eq nimp (nested_imp2nimp y) x))) (ni : nested_imps) (_ : my_nth nimp (S n) (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) ni y) (@eq nimp (nested_imp2nimp y) x)) *)
simpl in |- *; intros y ni nth.
(* Goal: @sig nested_imp (fun y0 : nested_imp => and (my_nth nested_imp O (@cons nested_imp y ni) y0) (@eq nimp (nested_imp2nimp y0) x)) *)
(* Goal: forall (n : nat) (_ : forall (ni : nested_imps) (_ : my_nth nimp n (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp n ni y) (@eq nimp (nested_imp2nimp y) x))) (ni : nested_imps) (_ : my_nth nimp (S n) (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) ni y) (@eq nimp (nested_imp2nimp y) x)) *)
exists y.
(* Goal: and (my_nth nested_imp (S n) (@cons nested_imp y ni) y') (@eq nimp (nested_imp2nimp y') x) *)
(* Goal: my_nth nimp n (nested_imps2nimps ni) x *)
split.
(* Goal: my_nth nested_imp O (@cons nested_imp y ni) y *)
(* Goal: @eq nimp (nested_imp2nimp y) x *)
(* Goal: forall (n : nat) (_ : forall (ni : nested_imps) (_ : my_nth nimp n (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp n ni y) (@eq nimp (nested_imp2nimp y) x))) (ni : nested_imps) (_ : my_nth nimp (S n) (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) ni y) (@eq nimp (nested_imp2nimp y) x)) *)
apply My_NthO.
(* Goal: forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NDisj a0 a1)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps (rev_app dni NNil)) x), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
inversion_clear nth.
(* Goal: @eq nimp (nested_imp2nimp y) (nested_imp2nimp y) *)
(* Goal: forall (n : nat) (_ : forall (ni : nested_imps) (_ : my_nth nimp n (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp n ni y) (@eq nimp (nested_imp2nimp y) x))) (ni : nested_imps) (_ : my_nth nimp (S n) (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) ni y) (@eq nimp (nested_imp2nimp y) x)) *)
trivial.
(* Goal: forall (n : nat) (_ : forall (ni : nested_imps) (_ : my_nth nimp n (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp n ni y) (@eq nimp (nested_imp2nimp y) x))) (ni : nested_imps) (_ : my_nth nimp (S n) (nested_imps2nimps ni) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) ni y) (@eq nimp (nested_imp2nimp y) x)) *)
intros n ih ni.
(* Goal: forall _ : my_nth nimp (S n) (nested_imps2nimps ni) x, @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) ni y) (@eq nimp (nested_imp2nimp y) x)) *)
case ni; clear ni.
(* Goal: forall _ : my_nth nimp (S n) (nested_imps2nimps (@nil nested_imp)) x, @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) (@nil nested_imp) y) (@eq nimp (nested_imp2nimp y) x)) *)
(* Goal: forall (n0 : nested_imp) (l : list nested_imp) (_ : my_nth nimp (S n) (nested_imps2nimps (@cons nested_imp n0 l)) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) (@cons nested_imp n0 l) y) (@eq nimp (nested_imp2nimp y) x)) *)
intros nth; elimtype False; inversion_clear nth.
(* Goal: forall (n0 : nested_imp) (l : list nested_imp) (_ : my_nth nimp (S n) (nested_imps2nimps (@cons nested_imp n0 l)) x), @sig nested_imp (fun y : nested_imp => and (my_nth nested_imp (S n) (@cons nested_imp n0 l) y) (@eq nimp (nested_imp2nimp y) x)) *)
intros y ni nth.        
(* Goal: @sig nested_imp (fun y0 : nested_imp => and (my_nth nested_imp (S n) (@cons nested_imp y ni) y0) (@eq nimp (nested_imp2nimp y0) x)) *)
elim (ih ni).
(* Goal: forall (x0 : nested_imp) (_ : and (my_nth nested_imp n ni x0) (@eq nimp (nested_imp2nimp x0) x)), @sig nested_imp (fun y0 : nested_imp => and (my_nth nested_imp (S n) (@cons nested_imp y ni) y0) (@eq nimp (nested_imp2nimp y0) x)) *)
(* Goal: my_nth nimp n (nested_imps2nimps ni) x *)
intros y' nth'.
(* Goal: @sig nested_imp (fun y0 : nested_imp => and (my_nth nested_imp (S n) (@cons nested_imp y ni) y0) (@eq nimp (nested_imp2nimp y0) x)) *)
(* Goal: my_nth nimp n (nested_imps2nimps ni) x *)
exists y'.
(* Goal: and (my_nth nested_imp (S n) (@cons nested_imp y ni) y') (@eq nimp (nested_imp2nimp y') x) *)
(* Goal: my_nth nimp n (nested_imps2nimps ni) x *)
elim nth'; clear nth'; intros nth' eq.
(* Goal: and (my_nth nested_imp (S n) (@cons nested_imp y ni) y') (@eq nimp (nested_imp2nimp y') x) *)
(* Goal: my_nth nimp n (nested_imps2nimps ni) x *)
split.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply My_NthS; assumption.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
inversion_clear nth; assumption.
Qed.

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

Lemma cons_counter_model :
 forall (i : Int) (dni : decorated_nested_imps) (ai : atomic_imps)
   (a : atoms),
 deco_sound nf_nil DNil (rev_app dni NNil) ai a ->
 a_ai_disj a ai ->
 a_goal_disj a i -> Cons_Counter_Model_Spec i (rev_app dni NNil) ai a.
(* Goal: forall (i : Int) (dni : decorated_nested_imps) (ai : atomic_imps) (a : atoms) (_ : deco_sound nf_nil DNil (rev_app dni NNil) ai a) (_ : a_ai_disj a ai) (_ : a_goal_disj a i), Cons_Counter_Model_Spec i (rev_app dni NNil) ai a *)
intros i dni ai a complete a_ai_disjunct a_goal_disj.
(* Goal: Cons_Counter_Model_Spec i (rev_app dni NNil) ai a *)
cut (Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil)))).
(* Goal: forall _ : Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))), Cons_Counter_Model_Spec i (rev_app dni NNil) ai a *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intro mon.
(* Goal: Cons_Counter_Model_Spec i (rev_app dni NNil) ai a *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
exists (node atoms a (n2forest (rev_app dni NNil))).

(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
(* Goal: forces_ngamma nf_nil DNil (rev_app dni NNil) ai a (node atoms a (n2forest (rev_app dni NNil))) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply mon.

(* Goal: forces_ngamma nf_nil DNil (rev_app dni NNil) ai a (node atoms a (n2forest (rev_app dni NNil))) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
unfold forces_ngamma in |- *.
(* Goal: forall (c : normal_form) (_ : in_ngamma nf_nil DNil (rev_app dni NNil) ai a c), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form c) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros c in_c.
(* Goal: forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form c) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
elim in_c; clear in_c c.

(* Goal: forall (n : nat) (c : normal_form) (_ : my_nth normal_form n nf_nil c), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form c) *)
(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n DNil (@pair Int Int i j)), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NDisj i j)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps (rev_app dni NNil)) x), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros n c nth.
(* Goal: forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NDisj a0 a1)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps (rev_app dni NNil)) x), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
inversion_clear nth.

(* Goal: forall (n : nat) (i j : Int) (_ : my_nth disj n DNil (@pair Int Int i j)), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NDisj i j)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps (rev_app dni NNil)) x), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros n a0 a1 nth.
(* Goal: forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NDisj a0 a1)) *)
(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps (rev_app dni NNil)) x), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
inversion_clear nth.

(* Goal: forall (n : nat) (x : nimp) (_ : my_nth nimp n (nested_imps2nimps (rev_app dni NNil)) x), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros n x; case x; clear x.
(* Goal: forall (i i0 : Int) (n0 : normal_form) (_ : my_nth nimp n (nested_imps2nimps (rev_app dni NNil)) (NImp i i0 n0)), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NImp_NF (NImp i i0 n0))) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros a0 a1 b nth.
(* Goal: forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp j b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
simpl in |- *; apply forces_t_imp.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Imp (Atom a0) (Atom a1)), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form b) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros forces_a0a1.
(* Goal: forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form b) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Atom j) (nf2form b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
elimtype False.
(* Goal: False *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
elim (nth_nimp__nth_nested_imp (NImp a0 a1 b) n (rev_app dni NNil) nth).
(* Goal: forall (x : nested_imp) (_ : and (my_nth nested_imp n (rev_app dni NNil) x) (@eq nimp (nested_imp2nimp x) (NImp a0 a1 b))), False *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros x; case x; clear x.
(* Goal: forall (n0 : nimp) (_ : and (my_nth nested_imp n (rev_app dni NNil) (Undecorated n0)) (@eq nimp (nested_imp2nimp (Undecorated n0)) (NImp a0 a1 b))), False *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (_ : and (my_nth nested_imp n (rev_app dni NNil) (Decorated n0 k)) (@eq nimp (nested_imp2nimp (Decorated n0 k)) (NImp a0 a1 b))), False *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros x nth_x.
(* Goal: False *)
(* Goal: forall (n0 : nimp) (k : kripke_tree) (_ : and (my_nth nested_imp n (rev_app dni NNil) (Decorated n0 k)) (@eq nimp (nested_imp2nimp (Decorated n0 k)) (NImp a0 a1 b))), False *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply all_ref_rev_app_nil with dni x.
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (rev_app dni NNil) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply nth_in with n.
(* Goal: forall _ : False, False *)
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall _ : @In nested_imp (Undecorated x) (rev_app l NNil), False) (_ : @In nested_imp (Undecorated x) (rev_app (@cons decorated_nested_imp a l) NNil)), False *)
elim nth_x; intros; assumption.
(* Goal: forall (n0 : nimp) (k : kripke_tree) (_ : and (my_nth nested_imp n (rev_app dni NNil) (Decorated n0 k)) (@eq nimp (nested_imp2nimp (Decorated n0 k)) (NImp a0 a1 b))), False *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros x k nth_x.
(* Goal: False *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
elim (complete k a0 a1 b).
(* Goal: forall (_ : Is_Monotone_kripke_tree k) (_ : forces_ngamma nf_nil DNil (rev_app dni NNil) ai a k) (_ : forall _ : forces_t k (Imp (Atom a0) (Atom a1)), False), False *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (rev_app dni NNil) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros k_is_mon k_forces_ngamma k_notforces_a0a1.
(* Goal: False *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (rev_app dni NNil) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply k_notforces_a0a1. 
(* Goal: forces_t k (Imp (Atom a0) (Atom a1)) *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (rev_app dni NNil) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply forces_t_mon with (node atoms a (n2forest (rev_app dni NNil))).
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: Suc k (node atoms a (n2forest (rev_app dni NNil))) *)
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (rev_app dni NNil) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply cons_counter_model_suc with x.
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (rev_app dni NNil) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply nth_in with n.
(* Goal: forall _ : False, False *)
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall _ : @In nested_imp (Undecorated x) (rev_app l NNil), False) (_ : @In nested_imp (Undecorated x) (rev_app (@cons decorated_nested_imp a l) NNil)), False *)
elim nth_x; intros; assumption.
(* Goal: @In nested_imp (Decorated (NImp a0 a1 b) k) (rev_app dni NNil) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply nth_in with n.
(* Goal: my_nth nested_imp n (rev_app dni NNil) (Decorated (NImp a0 a1 b) k) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
elim nth_x; clear nth_x; intros nth_x eq.
(* Goal: my_nth nested_imp n (rev_app dni NNil) (Decorated (NImp a0 a1 b) k) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
 rewrite <- eq.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Atom j) (nf2form b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
simpl in |- *.
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (n2forest (rev_app dni NNil))), forces_t k' (Imp (Atom j) (nf2form b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros k' in_k'.
(* Goal: forces_t k' (Imp (Imp (Atom a0) (Atom a1)) (nf2form b)) *)
(* 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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
change (forces_t k' (nf2form (NImp_NF (NImp a0 a1 b)))) in |- *.
(* Goal: forces_t k' (nf2form (AImp j b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply deco_sound_in_forest_forces with nf_nil DNil (rev_app dni NNil) ai a.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
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), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp i b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros j b n bs lookup_j nth.
(* Goal: forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (AImp j b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
simpl in |- *; apply forces_t_imp.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom j), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form b) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Atom j) (nf2form b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros forces_j.
(* Goal: forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form b) *)
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Atom j) (nf2form b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
elimtype False.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply a_ai_disjunct with j bs; assumption.
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (Succs (node atoms a (n2forest (rev_app dni NNil))))), forces_t k' (Imp (Atom j) (nf2form b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
simpl in |- *.
(* Goal: forall (k' : kripke_tree) (_ : In_Forest atoms k' (n2forest (rev_app dni NNil))), forces_t k' (Imp (Atom j) (nf2form b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros k' in_k'.
(* Goal: forces_t k' (Imp (Atom j) (nf2form b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
change (forces_t k' (nf2form (AImp j b))) in |- *.
(* Goal: forces_t k' (nf2form (AImp j b)) *)
(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply deco_sound_in_forest_forces with nf_nil DNil (rev_app dni NNil) ai a.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply In_Atomic_Imps with (i := j) (b := b) (n := n) (bs := bs); assumption.

(* Goal: forall (i : Int) (_ : LOOKUP unit i a tt), forces_t (node atoms a (n2forest (rev_app dni NNil))) (nf2form (NAtom i)) *)
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
intros j lookup_j.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.

(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
assumption.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply cons_counter_model_mon with ai; try assumption.
(* Goal: forall (x : nimp) (_ : @In nested_imp (Undecorated x) (rev_app dni NNil)), False *)
intros x in_x.
(* Goal: forall _ : forces_t (node atoms a (n2forest (rev_app dni NNil))) (Atom i), False *)
(* Goal: Is_Monotone_kripke_tree (node atoms a (n2forest (rev_app dni NNil))) *)
apply all_ref_rev_app_nil with dni x; assumption.
Qed.


