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



Require Export Rev_App.



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



Inductive le_ni : nested_imps -> nested_imps -> Prop :=
  | Le_NI_Nil : le_ni NNil NNil
  | Le_NI_Cons_NN :
      forall (x : nimp) (ni1 ni2 : nested_imps),
      le_ni ni1 ni2 -> le_ni (Undecorated x :: ni1) (Undecorated x :: ni2)
  | Le_NI_Cons_DN :
      forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps),
      le_ni ni1 ni2 -> le_ni (Decorated x k :: ni1) (Undecorated x :: ni2)
  | Le_NI_Cons_DD :
      forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps),
      le_ni ni1 ni2 -> le_ni (Decorated x k :: ni1) (Decorated x k :: ni2).






Lemma in_k_le :
 forall (ni1 ni2 : nested_imps) (x : nimp) (k : kripke_tree),
 le_ni ni1 ni2 -> In (Decorated x k) ni2 -> In (Decorated x k) ni1.
(* Goal: forall (ni1 ni2 : nested_imps) (x : nimp) (k : kripke_tree) (_ : le_ni ni1 ni2) (_ : @In nested_imp (Decorated x k) ni2), @In nested_imp (Decorated x k) ni1 *)
intros ni1 ni2 x k le12.
(* Goal: forall (ni3 : nested_imps) (_ : le_ni ni2 ni3), le_ni ni1 ni3 *)
elim le12; clear le12 ni1 ni2.
(* Goal: forall (ni3 : nested_imps) (_ : eqv_ni NNil ni3), eqv_ni NNil ni3 *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
intros; assumption.

(* Goal: forall (x0 : nimp) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : forall _ : @In nested_imp (Decorated x k) ni2, @In nested_imp (Decorated x k) ni1) (_ : @In nested_imp (Decorated x k) (@cons nested_imp (Undecorated x0) ni2)), @In nested_imp (Decorated x k) (@cons nested_imp (Undecorated x0) ni1) *)
(* Goal: forall (x0 : nimp) (k0 : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : forall _ : @In nested_imp (Decorated x k) ni2, @In nested_imp (Decorated x k) ni1) (_ : @In nested_imp (Decorated x k) (@cons nested_imp (Undecorated x0) ni2)), @In nested_imp (Decorated x k) (@cons nested_imp (Decorated x0 k0) ni1) *)
(* Goal: forall (x0 : nimp) (k0 : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : forall _ : @In nested_imp (Decorated x k) ni2, @In nested_imp (Decorated x k) ni1) (_ : @In nested_imp (Decorated x k) (@cons nested_imp (Decorated x0 k0) ni2)), @In nested_imp (Decorated x k) (@cons nested_imp (Decorated x0 k0) ni1) *)
intros x' ni1 ni2 le12 ih in_k.
(* Goal: @In nested_imp (Decorated x k) (@cons nested_imp (Decorated x' k') ni1) *)
(* Goal: forall (x0 : nimp) (k0 : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : forall _ : @In nested_imp (Decorated x k) ni2, @In nested_imp (Decorated x k) ni1) (_ : @In nested_imp (Decorated x k) (@cons nested_imp (Decorated x0 k0) ni2)), @In nested_imp (Decorated x k) (@cons nested_imp (Decorated x0 k0) ni1) *)
right.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: forces_t k (Atom i) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : filter_deco_spec i l), filter_deco_spec i (@cons nested_imp a l) *)
inversion_clear in_k.
(* Goal: forces_t k' (Atom i) *)
(* Goal: forces_t k' (Atom i) *)
 discriminate H.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.

(* Goal: forall (x0 : nimp) (k0 : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : forall _ : @In nested_imp (Decorated x k) ni2, @In nested_imp (Decorated x k) ni1) (_ : @In nested_imp (Decorated x k) (@cons nested_imp (Decorated x0 k0) ni2)), @In nested_imp (Decorated x k) (@cons nested_imp (Decorated x0 k0) ni1) *)
intros x' k' ni1 ni2 le12 ih in_k.
(* Goal: @In nested_imp (Decorated x k) (@cons nested_imp (Decorated x' k') ni1) *)
(* Goal: forall (x0 : nimp) (k0 : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : forall _ : @In nested_imp (Decorated x k) ni2, @In nested_imp (Decorated x k) ni1) (_ : @In nested_imp (Decorated x k) (@cons nested_imp (Decorated x0 k0) ni2)), @In nested_imp (Decorated x k) (@cons nested_imp (Decorated x0 k0) ni1) *)
right.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: forces_t k (Atom i) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : filter_deco_spec i l), filter_deco_spec i (@cons nested_imp a l) *)
inversion_clear in_k.
(* Goal: forces_t k' (Atom i) *)
(* Goal: forces_t k' (Atom i) *)
 discriminate H.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.

(* Goal: forall (x0 : nimp) (k0 : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : forall _ : @In nested_imp (Decorated x k) ni2, @In nested_imp (Decorated x k) ni1) (_ : @In nested_imp (Decorated x k) (@cons nested_imp (Decorated x0 k0) ni2)), @In nested_imp (Decorated x k) (@cons nested_imp (Decorated x0 k0) ni1) *)
intros x' k' ni1 ni2 le12 ih in_k.
(* Goal: forces_t k (Atom i) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : filter_deco_spec i l), filter_deco_spec i (@cons nested_imp a l) *)
inversion_clear in_k.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
left; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
right; apply ih; assumption.
Qed.




Lemma le_ni_refl : forall ni : nested_imps, le_ni ni ni.
(* Goal: forall ni : nested_imps, le_ni ni ni *)
intros ni; elim ni; clear ni.
(* Goal: le_ni NNil NNil *)
(* Goal: eqv_ni NNil NNil *)
(* Goal: forall (x : nimp) (k : kripke_tree) (_ : @In nested_imp (Decorated x k) NNil), or (@In nested_imp (Decorated x k) NNil) (@In nested_imp (Decorated x k) NNil) *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
apply Le_NI_Nil.
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l) *)
intros a; case a; clear a.
(* Goal: forall (n : nimp) (l : list nested_imp) (_ : le_ni l l), le_ni (@cons nested_imp (Undecorated n) l) (@cons nested_imp (Undecorated n) l) *)
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list nested_imp) (_ : le_ni l l), le_ni (@cons nested_imp (Decorated n k) l) (@cons nested_imp (Decorated n k) l) *)
intros x N ih.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Le_NI_Cons_NN; assumption.
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list nested_imp) (_ : filter_deco_spec i l), filter_deco_spec i (@cons nested_imp (Decorated n k) l) *)
intros x k ni ih.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Le_NI_Cons_DD; assumption.
Qed.




Lemma le_ni_trans :
 forall ni1 ni2 ni3 : nested_imps,
 le_ni ni1 ni2 -> le_ni ni2 ni3 -> le_ni ni1 ni3.
(* Goal: forall (ni1 ni2 ni3 : nested_imps) (_ : le_ni ni1 ni2) (_ : le_ni ni2 ni3), le_ni ni1 ni3 *)
intros ni1 ni2 ni3 le12.
(* Goal: forall (_ : @eq nat (@length nested_imp ni1) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
generalize ni3; clear ni3.
(* Goal: forall (ni3 : nested_imps) (_ : le_ni ni2 ni3), le_ni ni1 ni3 *)
elim le12; clear le12 ni1 ni2.
(* Goal: forall (ni3 : nested_imps) (_ : eqv_ni NNil ni3), eqv_ni NNil ni3 *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
intros; assumption.
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : le_ni ni2 ni3), le_ni ni1 ni3) (ni3 : nested_imps) (_ : le_ni (@cons nested_imp (Undecorated x) ni2) ni3), le_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : le_ni ni2 ni3), le_ni ni1 ni3) (ni3 : nested_imps) (_ : le_ni (@cons nested_imp (Undecorated x) ni2) ni3), le_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : le_ni ni2 ni3), le_ni ni1 ni3) (ni3 : nested_imps) (_ : le_ni (@cons nested_imp (Decorated x k) ni2) ni3), le_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
intros x ni1 ni2 le12 ih ni3 le23.
(* Goal: le_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
inversion_clear le23.
(* Goal: le_ni (@cons nested_imp (Undecorated x0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Undecorated x0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Undecorated x0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
apply Le_NI_Cons_NN.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply ih; assumption.
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : le_ni ni2 ni3), le_ni ni1 ni3) (ni3 : nested_imps) (_ : le_ni (@cons nested_imp (Decorated x k) ni2) ni3), le_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
intros x k ni1 ni2 le12 ih ni3 le23.
(* Goal: le_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
inversion_clear le23.
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Undecorated x0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
apply Le_NI_Cons_DN.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply ih; assumption.
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : le_ni ni2 ni3), le_ni ni1 ni3) (ni3 : nested_imps) (_ : le_ni (@cons nested_imp (Decorated x k) ni2) ni3), le_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
intros x k ni1 ni2 le12 ih ni3 le23.
(* Goal: le_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
inversion_clear le23.
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Undecorated x0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
apply Le_NI_Cons_DN.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply ih; assumption.
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
apply Le_NI_Cons_DD.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply ih; assumption.
Qed.





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


Inductive filter_deco_spec (i : Int) (N : nested_imps) : Set :=
    Filter_Deco_Spec_Intro :
      forall ni1 : nested_imps,
      le_ni N ni1 ->
      (forall (x : nimp) (k : kripke_tree),
       In (Decorated x k) ni1 -> forces_t k (Atom i)) -> 
      filter_deco_spec i N.


Lemma filter_deco :
 forall (i : Int) (ni : nested_imps), filter_deco_spec i ni.
(* Goal: forall (i : Int) (ni : nested_imps), filter_deco_spec i ni *)
intros i ni.
(* Goal: filter_deco_spec i ni *)
elim ni; clear ni.
(* Goal: filter_deco_spec i (@nil nested_imp) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : filter_deco_spec i l), filter_deco_spec i (@cons nested_imp a l) *)
fold NNil in |- *.
(* Goal: filter_deco_spec i NNil *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : filter_deco_spec i l), filter_deco_spec i (@cons nested_imp a l) *)
apply Filter_Deco_Spec_Intro with NNil.
(* Goal: le_ni NNil NNil *)
(* Goal: eqv_ni NNil NNil *)
(* Goal: forall (x : nimp) (k : kripke_tree) (_ : @In nested_imp (Decorated x k) NNil), or (@In nested_imp (Decorated x k) NNil) (@In nested_imp (Decorated x k) NNil) *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
apply Le_NI_Nil.
(* Goal: forall (x : nimp) (k : kripke_tree) (_ : @In nested_imp (Decorated x k) NNil), forces_t k (Atom i) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : filter_deco_spec i l), filter_deco_spec i (@cons nested_imp a l) *)
intros x k in_k.
(* Goal: forces_t k (Atom i) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : filter_deco_spec i l), filter_deco_spec i (@cons nested_imp a l) *)
inversion_clear in_k. 

(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l) *)
intros a; case a; clear a.
(* Goal: forall (n : nimp) (l : list nested_imp) (_ : filter_deco_spec i l), filter_deco_spec i (@cons nested_imp (Undecorated n) l) *)
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list nested_imp) (_ : filter_deco_spec i l), filter_deco_spec i (@cons nested_imp (Decorated n k) l) *)
intros x ni ih.
(* Goal: inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
elim ih; clear ih.
(* Goal: forall (ni1 : nested_imps) (_ : le_ni ni ni1) (_ : forall (x : nimp) (k : kripke_tree) (_ : @In nested_imp (Decorated x k) ni1), forces_t k (Atom i)), filter_deco_spec i (@cons nested_imp (Decorated x k) ni) *)
intros ni1 le1 forces_i.
(* Goal: filter_deco_spec i (@cons nested_imp (Decorated x (node atoms (AVL_intro unit t avl_t) succs)) ni) *)
apply Filter_Deco_Spec_Intro with (Undecorated x :: ni1).
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Le_NI_Cons_NN; assumption.
(* Goal: forall (x0 : nimp) (k0 : kripke_tree) (_ : @In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni)), or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni2)) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
intros x' k' in_k0.
(* Goal: forces_t k' (Atom i) *)
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list nested_imp) (_ : filter_deco_spec i l), filter_deco_spec i (@cons nested_imp (Decorated n k) l) *)
apply forces_i with x'.
(* Goal: or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni2)) *)
inversion_clear in_k0.
(* Goal: forces_t k' (Atom i) *)
(* Goal: forces_t k' (Atom i) *)
 discriminate H.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.

(* Goal: forall (n : nimp) (k : kripke_tree) (l : list nested_imp) (_ : filter_deco_spec i l), filter_deco_spec i (@cons nested_imp (Decorated n k) l) *)
intros x k ni ih.
(* Goal: inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
elim ih; clear ih.
(* Goal: forall (ni1 : nested_imps) (_ : le_ni ni ni1) (_ : forall (x : nimp) (k : kripke_tree) (_ : @In nested_imp (Decorated x k) ni1), forces_t k (Atom i)), filter_deco_spec i (@cons nested_imp (Decorated x k) ni) *)
intros ni1 le1 forces_i.
(* Goal: filter_deco_spec i (@cons nested_imp (Decorated x k) ni) *)
case k; clear k.
(* Goal: forall (a : atoms) (f : Forest atoms), filter_deco_spec i (@cons nested_imp (Decorated x (node atoms a f)) ni) *)
intros Atms succs.
(* Goal: filter_deco_spec i (@cons nested_imp (Decorated x (node atoms Atms succs)) ni) *)
case Atms; clear Atms.
(* Goal: forall (t : avl_tree unit) (i0 : is_avl unit t), filter_deco_spec i (@cons nested_imp (Decorated x (node atoms (AVL_intro unit t i0) succs)) ni) *)
intros t avl_t.
(* Goal: filter_deco_spec i (@cons nested_imp (Decorated x (node atoms (AVL_intro unit t avl_t) succs)) ni) *)
elim (lookup_dec unit i t avl_t).
(* Goal: forall (d : unit) (_ : lookup unit i t d), filter_deco_spec i (@cons nested_imp (Decorated x (node atoms (AVL_intro unit t avl_t) succs)) ni) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i t d), filter_deco_spec i (@cons nested_imp (Decorated x (node atoms (AVL_intro unit t avl_t) succs)) ni) *)
intros d; case d; clear d.
(* Goal: forall _ : lookup unit i t tt, filter_deco_spec i (@cons nested_imp (Decorated x (node atoms (AVL_intro unit t avl_t) succs)) ni) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i t d), filter_deco_spec i (@cons nested_imp (Decorated x (node atoms (AVL_intro unit t avl_t) succs)) ni) *)
intros lookup.
apply
 Filter_Deco_Spec_Intro
  with (Decorated x (node atoms (AVL_intro unit t avl_t) succs) :: ni1).
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Le_NI_Cons_DD; assumption.
(* Goal: forall (x0 : nimp) (k0 : kripke_tree) (_ : @In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni)), or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni2)) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
intros x' k' in_k0.
(* Goal: or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni2)) *)
inversion_clear in_k0.
(* Goal: forces_t k' (Atom i) *)
(* Goal: forces_t k' (Atom i) *)
(* Goal: forall _ : forall d : unit, not (lookup unit i t d), filter_deco_spec i (@cons nested_imp (Decorated x (node atoms (AVL_intro unit t avl_t) succs)) ni) *)
 injection H; clear H; intros.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
 rewrite <- H; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply forces_i with x'; assumption.

(* Goal: forall _ : forall d : unit, not (lookup unit i t d), filter_deco_spec i (@cons nested_imp (Decorated x (node atoms (AVL_intro unit t avl_t) succs)) ni) *)
intros notlookup.
(* Goal: filter_deco_spec i (@cons nested_imp (Decorated x (node atoms (AVL_intro unit t avl_t) succs)) ni) *)
apply Filter_Deco_Spec_Intro with (Undecorated x :: ni1).
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Le_NI_Cons_DN; assumption.
(* Goal: forall (x0 : nimp) (k0 : kripke_tree) (_ : @In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni)), or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni2)) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
simpl in |- *; intros x' k' in_k0.
(* Goal: or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni2)) *)
inversion_clear in_k0.
(* Goal: forces_t k' (Atom i) *)
(* Goal: forces_t k' (Atom i) *)
 discriminate H.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply forces_i with x'; assumption.
Qed.


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


Inductive eqv_ni : nested_imps -> nested_imps -> Prop :=
  | Eqv_NI_Nil : eqv_ni NNil NNil
  | Eqv_NI_Cons_NN :
      forall (x : nimp) (ni1 ni2 : nested_imps),
      eqv_ni ni1 ni2 -> eqv_ni (Undecorated x :: ni1) (Undecorated x :: ni2)
  | Eqv_NI_Cons_DN :
      forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps),
      eqv_ni ni1 ni2 -> eqv_ni (Decorated x k :: ni1) (Undecorated x :: ni2)
  | Eqv_NI_Cons_DD :
      forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps),
      eqv_ni ni1 ni2 -> eqv_ni (Decorated x k :: ni1) (Decorated x k' :: ni2)
  | Eqv_NI_Cons_ND :
      forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps),
      eqv_ni ni1 ni2 -> eqv_ni (Undecorated x :: ni1) (Decorated x k :: ni2).



Lemma eqv_ni_trans :
 forall ni1 ni2 ni3 : nested_imps,
 eqv_ni ni1 ni2 -> eqv_ni ni2 ni3 -> eqv_ni ni1 ni3.
(* Goal: forall (ni1 ni2 ni3 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3 *)
intros ni1 ni2 ni3 eqv12.
(* Goal: forall (_ : @eq nat (@length nested_imp ni1) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
generalize ni3; clear ni3.
(* Goal: inf_deco_spec ni1 ni2 *)
elim eqv12; clear eqv12 ni1 ni2.
(* Goal: forall (ni3 : nested_imps) (_ : eqv_ni NNil ni3), eqv_ni NNil ni3 *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
intros; assumption.
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
intros x ni1 ni2 eqv12 ih ni3 eqv23.
(* Goal: eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
inversion_clear eqv23.
(* Goal: eqv_ni (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Undecorated x) ni4) *)
(* Goal: eqv_ni (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k') ni4) *)
apply Eqv_NI_Cons_NN.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply ih; assumption.
(* Goal: eqv_ni (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k') ni4) *)
apply Eqv_NI_Cons_ND.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply ih; assumption.
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
intros x k ni1 ni2 eqv12 ih ni3 eqv23.
(* Goal: eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
inversion_clear eqv23.
(* Goal: eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated x) ni4) *)
(* Goal: eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k'0) ni4) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
apply Eqv_NI_Cons_DN.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply ih; assumption.
(* Goal: eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k'0) ni4) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
apply Eqv_NI_Cons_DD.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply ih; assumption.
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
intros x k k' ni1 ni2 eqv12 ih ni3 eqv23.
(* Goal: eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
inversion_clear eqv23.
(* Goal: eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated x) ni4) *)
(* Goal: eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k'0) ni4) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
apply Eqv_NI_Cons_DN.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply ih; assumption.
(* Goal: eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k'0) ni4) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
apply Eqv_NI_Cons_DD.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply ih; assumption.
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
intros x k ni1 ni2 eqv12 ih ni3 eqv23.
(* Goal: eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
inversion_clear eqv23.
(* Goal: eqv_ni (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Undecorated x) ni4) *)
(* Goal: eqv_ni (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k') ni4) *)
apply Eqv_NI_Cons_NN.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply ih; assumption.
(* Goal: eqv_ni (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k') ni4) *)
apply Eqv_NI_Cons_ND.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply ih; assumption.
Qed.


Lemma le_eqv : forall ni1 ni2 : nested_imps, le_ni ni1 ni2 -> eqv_ni ni1 ni2.
(* Goal: forall (ni3 : nested_imps) (_ : le_ni ni2 ni3), le_ni ni1 ni3 *)
intros ni1 ni2 le12; elim le12; clear le12 ni1 ni2.
(* Goal: eqv_ni NNil NNil *)
(* Goal: forall (x : nimp) (k : kripke_tree) (_ : @In nested_imp (Decorated x k) NNil), or (@In nested_imp (Decorated x k) NNil) (@In nested_imp (Decorated x k) NNil) *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
apply Eqv_NI_Nil.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros x ni1 ni2 le12 ih; apply Eqv_NI_Cons_NN; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros x k ni1 ni2 le12 ih; apply Eqv_NI_Cons_DN; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros x k ni1 ni2 le12 ih; apply Eqv_NI_Cons_DD; assumption.
Qed.


Lemma eqv_sym :
 forall ni1 ni2 : nested_imps, eqv_ni ni1 ni2 -> eqv_ni ni2 ni1.
(* Goal: inf_deco_spec ni1 ni2 *)
intros ni1 ni2 eqv12; elim eqv12; clear eqv12 ni1 ni2.
(* Goal: eqv_ni NNil NNil *)
(* Goal: forall (x : nimp) (k : kripke_tree) (_ : @In nested_imp (Decorated x k) NNil), or (@In nested_imp (Decorated x k) NNil) (@In nested_imp (Decorated x k) NNil) *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
apply Eqv_NI_Nil.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros x ni1 ni2 eqv12 ih; apply Eqv_NI_Cons_NN; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros x k ni1 ni2 eqv12 ih; apply Eqv_NI_Cons_ND; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros x k k' ni1 ni2 eqv12 ih; apply Eqv_NI_Cons_DD; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros x k ni1 ni2 eqv12 ih; apply Eqv_NI_Cons_DN; assumption.
Qed.


Lemma ge_eqv : forall ni1 ni2 : nested_imps, le_ni ni2 ni1 -> eqv_ni ni1 ni2.
(* Goal: forall (ni1 ni2 : nested_imps) (_ : le_ni ni2 ni1), eqv_ni ni1 ni2 *)
intros ni1 ni2 le21.
(* Goal: eqv_ni ni1 ni2 *)
apply eqv_sym.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply le_eqv; assumption.
Qed.

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

Lemma eqv_ni_rec :
 forall P : nested_imps -> nested_imps -> Set,
 P NNil NNil ->
 (forall (x : nimp) (ni1 ni2 : nested_imps),
  eqv_ni ni1 ni2 ->
  P ni1 ni2 -> P (Undecorated x :: ni1) (Undecorated x :: ni2)) ->
 (forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps),
  eqv_ni ni1 ni2 ->
  P ni1 ni2 -> P (Decorated x k :: ni1) (Undecorated x :: ni2)) ->
 (forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps),
  eqv_ni ni1 ni2 ->
  P ni1 ni2 -> P (Decorated x k :: ni1) (Decorated x k' :: ni2)) ->
 (forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps),
  eqv_ni ni1 ni2 ->
  P ni1 ni2 -> P (Undecorated x :: ni1) (Decorated x k :: ni2)) ->
 forall ni1 ni2 : nested_imps, eqv_ni ni1 ni2 -> P ni1 ni2.
(* Goal: forall (P : forall (_ : nested_imps) (_ : nested_imps), Set) (_ : P NNil NNil) (_ : forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : P ni1 ni2), P (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Undecorated x) ni2)) (_ : forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : P ni1 ni2), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated x) ni2)) (_ : forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : P ni1 ni2), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2)) (_ : forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : P ni1 ni2), P (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2)) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2), P ni1 ni2 *)
intros P base step_nn step_rn step_rr step_nr ni1.
(* Goal: forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp ni1) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
elim ni1; clear ni1.
(* Goal: forall (ni2 : nested_imps) (_ : eqv_ni (@nil nested_imp) ni2), P (@nil nested_imp) ni2 *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni2 : nested_imps) (_ : eqv_ni l ni2), P l ni2) (ni2 : nested_imps) (_ : eqv_ni (@cons nested_imp a l) ni2), P (@cons nested_imp a l) ni2 *)
intros ni2; case ni2; clear ni2.
(* Goal: forall _ : eqv_ni (@nil nested_imp) (@nil nested_imp), P (@nil nested_imp) (@nil nested_imp) *)
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : eqv_ni (@nil nested_imp) (@cons nested_imp n l)), P (@nil nested_imp) (@cons nested_imp n l) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni2 : nested_imps) (_ : eqv_ni l ni2), P l ni2) (ni2 : nested_imps) (_ : eqv_ni (@cons nested_imp a l) ni2), P (@cons nested_imp a l) ni2 *)
intros; apply base.
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : eqv_ni (@nil nested_imp) (@cons nested_imp n l)), P (@nil nested_imp) (@cons nested_imp n l) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni2 : nested_imps) (_ : eqv_ni l ni2), P l ni2) (ni2 : nested_imps) (_ : eqv_ni (@cons nested_imp a l) ni2), P (@cons nested_imp a l) ni2 *)
intros a ni2 eqv; elimtype False; inversion_clear eqv.


(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l) *)
intros a; case a; clear a.
(* Goal: forall (n : nimp) (l : list nested_imp) (_ : forall (ni2 : nested_imps) (_ : eqv_ni l ni2), P l ni2) (ni2 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated n) l) ni2), P (@cons nested_imp (Undecorated n) l) ni2 *)
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni2 : nested_imps) (_ : eqv_ni l ni2), P l ni2) (ni2 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated n k) l) ni2), P (@cons nested_imp (Decorated n k) l) ni2 *)
intros x ni1 ih ni2.
(* Goal: forall _ : eqv_ni (@cons nested_imp (Decorated x k) ni1) ni2, P (@cons nested_imp (Decorated x k) ni1) ni2 *)
case ni2; clear ni2.
(* Goal: forall _ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@nil nested_imp), P (@cons nested_imp (Decorated x k) ni1) (@nil nested_imp) *)
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l) *)
intros eqv; elimtype False; inversion_clear eqv.
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l) *)
intros a; case a; clear a.
(* Goal: forall (n : nimp) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated n) l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated n) l) *)
(* Goal: forall (n : nimp) (k0 : kripke_tree) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated n k0) l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated n k0) l) *)
intros x' ni2 eqv.
(* Goal: P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x' k') ni2) *)
cut (x = x').
intro eq_x;  rewrite eq_x; clear eq_x.
(* Goal: P (@cons nested_imp (Undecorated x') ni1) (@cons nested_imp (Undecorated x') ni2) *)
(* Goal: @eq nimp x x' *)
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated n k) l)), P (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated n k) l) *)
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni2 : nested_imps) (_ : eqv_ni l ni2), P l ni2) (ni2 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated n k) l) ni2), P (@cons nested_imp (Decorated n k) l) ni2 *)
apply step_nn.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
inversion_clear eqv; assumption.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
inversion_clear eqv; assumption.
(* Goal: @eq nimp x x' *)
inversion_clear eqv; trivial.
(* Goal: forall (n : nimp) (k0 : kripke_tree) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated n k0) l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated n k0) l) *)
intros x' k' ni2 eqv.
(* Goal: P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x' k') ni2) *)
cut (x = x').
intro eq_x;  rewrite eq_x; clear eq_x.
(* Goal: P (@cons nested_imp (Undecorated x') ni1) (@cons nested_imp (Decorated x' k') ni2) *)
(* Goal: @eq nimp x x' *)
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni2 : nested_imps) (_ : eqv_ni l ni2), P l ni2) (ni2 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated n k) l) ni2), P (@cons nested_imp (Decorated n k) l) ni2 *)
apply step_nr.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
inversion_clear eqv; assumption.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
inversion_clear eqv; assumption.
(* Goal: @eq nimp x x' *)
inversion_clear eqv; trivial.

(* Goal: forall (n : nimp) (k : kripke_tree) (l : list nested_imp) (_ : forall (ni2 : nested_imps) (_ : eqv_ni l ni2), P l ni2) (ni2 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated n k) l) ni2), P (@cons nested_imp (Decorated n k) l) ni2 *)
intros x k ni1 ih ni2.
(* Goal: forall _ : eqv_ni (@cons nested_imp (Decorated x k) ni1) ni2, P (@cons nested_imp (Decorated x k) ni1) ni2 *)
case ni2; clear ni2.
(* Goal: forall _ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@nil nested_imp), P (@cons nested_imp (Decorated x k) ni1) (@nil nested_imp) *)
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l) *)
intros eqv; elimtype False; inversion_clear eqv.
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp n l) *)
intros a; case a; clear a.
(* Goal: forall (n : nimp) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated n) l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated n) l) *)
(* Goal: forall (n : nimp) (k0 : kripke_tree) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated n k0) l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated n k0) l) *)
intros x' ni2 eqv.
(* Goal: P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x' k') ni2) *)
cut (x = x').
intro eq_x;  rewrite eq_x; clear eq_x.
(* Goal: P (@cons nested_imp (Decorated x' k) ni1) (@cons nested_imp (Undecorated x') ni2) *)
(* Goal: @eq nimp x x' *)
(* Goal: forall (n : nimp) (k0 : kripke_tree) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated n k0) l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated n k0) l) *)
apply step_rn.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
inversion_clear eqv; assumption.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
inversion_clear eqv; assumption.
(* Goal: @eq nimp x x' *)
inversion_clear eqv; trivial.
(* Goal: forall (n : nimp) (k0 : kripke_tree) (l : list nested_imp) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated n k0) l)), P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated n k0) l) *)
intros x' k' ni2 eqv.
(* Goal: P (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x' k') ni2) *)
cut (x = x').
intro eq_x;  rewrite eq_x; clear eq_x.
(* Goal: P (@cons nested_imp (Decorated x' k) ni1) (@cons nested_imp (Decorated x' k') ni2) *)
(* Goal: @eq nimp x x' *)
apply step_rr.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
inversion_clear eqv; assumption.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
inversion_clear eqv; assumption.
(* Goal: @eq nimp x x' *)
inversion_clear eqv; trivial.
Qed.

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


Inductive inf_deco_spec (ni1 ni2 : nested_imps) : Set :=
    Inf_Deco_Spec_Intro :
      forall ni : nested_imps,
      le_ni ni ni1 ->
      eqv_ni ni ni2 ->
      (forall (x : nimp) (k : kripke_tree),
       In (Decorated x k) ni ->
       In (Decorated x k) ni1 \/ In (Decorated x k) ni2) ->
      inf_deco_spec ni1 ni2.


Lemma inf_deco :
 forall ni1 ni2 : nested_imps, eqv_ni ni1 ni2 -> inf_deco_spec ni1 ni2.
(* Goal: forall (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2), inf_deco_spec ni1 ni2 *)
intros ni1 ni2 eqv12. 
(* Goal: inf_deco_spec ni1 ni2 *)
elim eqv12; clear eqv12 ni1 ni2.
(* Goal: inf_deco_spec NNil NNil *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
apply Inf_Deco_Spec_Intro with NNil.
(* Goal: le_ni NNil NNil *)
(* Goal: eqv_ni NNil NNil *)
(* Goal: forall (x : nimp) (k : kripke_tree) (_ : @In nested_imp (Decorated x k) NNil), or (@In nested_imp (Decorated x k) NNil) (@In nested_imp (Decorated x k) NNil) *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
apply Le_NI_Nil.
(* Goal: eqv_ni NNil NNil *)
(* Goal: forall (x : nimp) (k : kripke_tree) (_ : @In nested_imp (Decorated x k) NNil), or (@In nested_imp (Decorated x k) NNil) (@In nested_imp (Decorated x k) NNil) *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
apply Eqv_NI_Nil.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros; left; assumption.

(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
intros x ni1 ni2 eqv12 ih.
(* Goal: inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
elim ih; clear ih.
(* Goal: forall (ni : nested_imps) (_ : le_ni ni ni1) (_ : eqv_ni ni ni2) (_ : forall (x : nimp) (k : kripke_tree) (_ : @In nested_imp (Decorated x k) ni), or (@In nested_imp (Decorated x k) ni1) (@In nested_imp (Decorated x k) ni2)), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
intros ni le eqv inf.
(* Goal: inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Undecorated x) ni2) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
apply Inf_Deco_Spec_Intro with (Undecorated x :: ni).
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Le_NI_Cons_NN; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Eqv_NI_Cons_NN; assumption.
(* Goal: forall (x0 : nimp) (k0 : kripke_tree) (_ : @In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni)), or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni2)) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
intros x' k' in_k0.
(* Goal: or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni2)) *)
inversion_clear in_k0.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
left; left; assumption.
(* Goal: or (@In nested_imp (Decorated x' k') (@cons nested_imp (Decorated x k) ni1)) (@In nested_imp (Decorated x' k') (@cons nested_imp (Undecorated x) ni2)) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
elim (inf x' k' H); clear inf H.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros in_ni1; left; right; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros in_ni2; right; right; assumption.

(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
intros x k ni1 ni2 eqv12 ih.
(* Goal: inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
elim ih; clear ih.
(* Goal: forall (ni : nested_imps) (_ : le_ni ni ni1) (_ : eqv_ni ni ni2) (_ : forall (x : nimp) (k : kripke_tree) (_ : @In nested_imp (Decorated x k) ni), or (@In nested_imp (Decorated x k) ni1) (@In nested_imp (Decorated x k) ni2)), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
intros ni le eqv inf.
(* Goal: inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
apply Inf_Deco_Spec_Intro with (Decorated x k :: ni).
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Le_NI_Cons_DD; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Eqv_NI_Cons_DN; assumption.
(* Goal: forall (x0 : nimp) (k0 : kripke_tree) (_ : @In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni)), or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni2)) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
intros x' k' in_k0.
(* Goal: or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni2)) *)
inversion_clear in_k0.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
left; left; assumption.
(* Goal: or (@In nested_imp (Decorated x' k') (@cons nested_imp (Decorated x k) ni1)) (@In nested_imp (Decorated x' k') (@cons nested_imp (Undecorated x) ni2)) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
elim (inf x' k' H); clear inf H.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros in_ni1; left; right; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros in_ni2; right; right; assumption.

(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Decorated x k) ni1) (@cons nested_imp (Decorated x k') ni2) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
intros x k k' ni1 ni2 eqv12 ih.
(* Goal: inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
elim ih; clear ih.
(* Goal: forall (ni : nested_imps) (_ : le_ni ni ni1) (_ : eqv_ni ni ni2) (_ : forall (x : nimp) (k : kripke_tree) (_ : @In nested_imp (Decorated x k) ni), or (@In nested_imp (Decorated x k) ni1) (@In nested_imp (Decorated x k) ni2)), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
intros ni le eqv inf.
(* Goal: inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
apply Inf_Deco_Spec_Intro with (Decorated x k :: ni).
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Le_NI_Cons_DD; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Eqv_NI_Cons_DD; assumption.
(* Goal: forall (x0 : nimp) (k0 : kripke_tree) (_ : @In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni)), or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni2)) *)
intros x0 k0 in_k0.
(* Goal: or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni2)) *)
inversion_clear in_k0.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
left; left; assumption.
(* Goal: or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni2)) *)
elim (inf x0 k0 H); clear inf H.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros in_ni1; left; right; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros in_ni2; right; right; assumption.


(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : inf_deco_spec ni1 ni2), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
intros x k ni1 ni2 eqv12 ih.
(* Goal: inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
elim ih; clear ih.
(* Goal: forall (ni : nested_imps) (_ : le_ni ni ni1) (_ : eqv_ni ni ni2) (_ : forall (x : nimp) (k : kripke_tree) (_ : @In nested_imp (Decorated x k) ni), or (@In nested_imp (Decorated x k) ni1) (@In nested_imp (Decorated x k) ni2)), inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
intros ni le eqv inf.
(* Goal: inf_deco_spec (@cons nested_imp (Undecorated x) ni1) (@cons nested_imp (Decorated x k) ni2) *)
apply Inf_Deco_Spec_Intro with (Decorated x k :: ni).
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Le_NI_Cons_DN; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Eqv_NI_Cons_DD; assumption.
(* Goal: forall (x0 : nimp) (k0 : kripke_tree) (_ : @In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni)), or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni2)) *)
intros x0 k0 in_k0.
(* Goal: or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni2)) *)
inversion_clear in_k0.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
right; left; assumption.
(* Goal: or (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Undecorated x) ni1)) (@In nested_imp (Decorated x0 k0) (@cons nested_imp (Decorated x k) ni2)) *)
elim (inf x0 k0 H); clear inf H.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros in_ni1; left; right; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
intros in_ni2; right; right; assumption.
Qed.


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

Remark eqv_nimps_eq :
 forall ni1 ni2 : nested_imps,
 eqv_ni ni1 ni2 -> nested_imps2nimps ni1 = nested_imps2nimps ni2.
(* Goal: forall (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2), @eq (list nimp) (nested_imps2nimps ni1) (nested_imps2nimps ni2) *)
intros ni1 ni2 eqv.
(* Goal: @eq (list nimp) (nested_imps2nimps ni1) (nested_imps2nimps ni2) *)
elim eqv; clear eqv ni1 ni2; simpl in |- *.
(* Goal: @Logic.eq nested_imps (@cons nested_imp x' (@app nested_imp ni11 ni12)) (@app nested_imp (@cons nested_imp x' ni11) ni12) *)
(* Goal: @Logic.eq nat (@length nested_imp (@cons nested_imp x' ni11)) (S (@length nested_imp ni21)) *)
(* Goal: le_ni ni1 (@app nested_imp ni21 ni22) *)
trivial.
(* Goal: @Logic.eq nested_imps (@cons nested_imp x' (@app nested_imp ni11 ni12)) (@app nested_imp (@cons nested_imp x' ni11) ni12) *)
(* Goal: @Logic.eq nat (@length nested_imp (@cons nested_imp x' ni11)) (S (@length nested_imp ni21)) *)
(* Goal: le_ni ni1 (@app nested_imp ni21 ni22) *)
intros x ni1 ni2 eqv ih;  rewrite ih; trivial.
(* Goal: @Logic.eq nested_imps (@cons nested_imp x' (@app nested_imp ni11 ni12)) (@app nested_imp (@cons nested_imp x' ni11) ni12) *)
(* Goal: @Logic.eq nat (@length nested_imp (@cons nested_imp x' ni11)) (S (@length nested_imp ni21)) *)
(* Goal: le_ni ni1 (@app nested_imp ni21 ni22) *)
intros x k ni1 ni2 eqv ih;  rewrite ih; trivial.
(* Goal: @Logic.eq nested_imps (@cons nested_imp x' (@app nested_imp ni11 ni12)) (@app nested_imp (@cons nested_imp x' ni11) ni12) *)
(* Goal: @Logic.eq nat (@length nested_imp (@cons nested_imp x' ni11)) (S (@length nested_imp ni21)) *)
(* Goal: le_ni ni1 (@app nested_imp ni21 ni22) *)
intros x k1 k2 ni1 ni2 eqv ih;  rewrite ih; trivial.
(* Goal: @Logic.eq nested_imps (@cons nested_imp x' (@app nested_imp ni11 ni12)) (@app nested_imp (@cons nested_imp x' ni11) ni12) *)
(* Goal: @Logic.eq nat (@length nested_imp (@cons nested_imp x' ni11)) (S (@length nested_imp ni21)) *)
(* Goal: le_ni ni1 (@app nested_imp ni21 ni22) *)
intros x k ni1 ni2 eqv ih;  rewrite ih; trivial.
Qed.


Lemma in_ngamma_eqv :
 forall (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps)
   (ai : atomic_imps) (a : atoms) (c : normal_form),
 eqv_ni ni1 ni2 ->
 in_ngamma work ds ni1 ai a c -> in_ngamma work ds ni2 ai a c.
(* Goal: forall (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : eqv_ni ni1 ni2) (_ : in_ngamma work ds ni1 ai a c), in_ngamma work ds ni2 ai a c *)
intros work ds ni1 ni2 ai a c eqv12 ini1.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply in_ngamma_ni_eq with ni1; try assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply eqv_nimps_eq; assumption.
Qed.



Lemma in_ngamma_le :
 forall (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps)
   (ai : atomic_imps) (a : atoms) (c : normal_form),
 le_ni ni1 ni2 ->
 in_ngamma work ds ni1 ai a c -> in_ngamma work ds ni2 ai a c.
(* Goal: forall (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : le_ni ni1 ni2) (_ : in_ngamma work ds ni1 ai a c), in_ngamma work ds ni2 ai a c *)
intros work ds ni1 ni2 ai a c le12 in_ngamma.
(* Goal: In_NGamma.in_ngamma work ds ni2 ai a c *)
apply in_ngamma_eqv with ni1.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply le_eqv; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.
Qed.

Lemma in_ngamma_ge :
 forall (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps)
   (ai : atomic_imps) (a : atoms) (c : normal_form),
 le_ni ni2 ni1 ->
 in_ngamma work ds ni1 ai a c -> in_ngamma work ds ni2 ai a c.
(* Goal: forall (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps) (ai : atomic_imps) (a : atoms) (c : normal_form) (_ : le_ni ni2 ni1) (_ : in_ngamma work ds ni1 ai a c), in_ngamma work ds ni2 ai a c *)
intros work ds ni1 ni2 ai a c le21 in_ngamma.
(* Goal: In_NGamma.in_ngamma work ds ni2 ai a c *)
apply in_ngamma_eqv with ni1.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply ge_eqv; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.
Qed.


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


Inductive le_app_spec (ni1 : nested_imps) (n : nat) : Set :=
    Le_App_Spec_Intro :
      forall ni11 ni12 : nested_imps,
      ni1 = ni11 ++ ni12 -> length ni11 = n -> le_app_spec ni1 n.

Lemma le_app0 :
 forall ni1 ni21 ni22 : nested_imps,
 le_ni ni1 (ni21 ++ ni22) -> le_app_spec ni1 (length ni21).
(* Goal: forall (ni1 ni21 ni22 : nested_imps) (_ : le_ni ni1 (@app nested_imp ni21 ni22)), le_app_spec ni1 (@length nested_imp ni21) *)
intros ni1 ni21 ni22.
(* Goal: forall _ : le_ni ni1 (@app nested_imp ni21 ni22), le_app_spec ni1 (@length nested_imp ni21) *)
generalize ni1; clear ni1.
(* Goal: forall (ni1 : nested_imps) (_ : le_ni ni1 (@app nested_imp ni21 ni22)), le_app_spec ni1 (@length nested_imp ni21) *)
elim ni21; clear ni21.
(* Goal: forall (ni1 : nested_imps) (_ : le_ni ni1 (@app nested_imp (@nil nested_imp) ni22)), le_app_spec ni1 (@length nested_imp (@nil nested_imp)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (_ : le_ni ni1 (@app nested_imp l ni22)), le_app_spec ni1 (@length nested_imp l)) (ni1 : nested_imps) (_ : le_ni ni1 (@app nested_imp (@cons nested_imp a l) ni22)), le_app_spec ni1 (@length nested_imp (@cons nested_imp a l)) *)
simpl in |- *; intros ni1 le.
(* Goal: le_app_spec ni1 O *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (_ : le_ni ni1 (@app nested_imp l ni22)), le_app_spec ni1 (@length nested_imp l)) (ni1 : nested_imps) (_ : le_ni ni1 (@app nested_imp (@cons nested_imp a l) ni22)), le_app_spec ni1 (@length nested_imp (@cons nested_imp a l)) *)
exists NNil ni1.
(* Goal: @Logic.eq nested_imps (@cons nested_imp x' (@app nested_imp ni11 ni12)) (@app nested_imp (@cons nested_imp x' ni11) ni12) *)
(* Goal: @Logic.eq nat (@length nested_imp (@cons nested_imp x' ni11)) (S (@length nested_imp ni21)) *)
(* Goal: le_ni ni1 (@app nested_imp ni21 ni22) *)
trivial.
(* Goal: @Logic.eq nested_imps (@cons nested_imp x' (@app nested_imp ni11 ni12)) (@app nested_imp (@cons nested_imp x' ni11) ni12) *)
(* Goal: @Logic.eq nat (@length nested_imp (@cons nested_imp x' ni11)) (S (@length nested_imp ni21)) *)
(* Goal: le_ni ni1 (@app nested_imp ni21 ni22) *)
trivial.
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni1 : nested_imps) (_ : le_ni ni1 (@app nested_imp l ni22)), le_app_spec ni1 (@length nested_imp l)) (ni1 : nested_imps) (_ : le_ni ni1 (@app nested_imp (@cons nested_imp a l) ni22)), le_app_spec ni1 (@length nested_imp (@cons nested_imp a l)) *)
intros x ni21 ih ni1.
(* Goal: forall _ : le_ni ni1 (@app nested_imp (@cons nested_imp x ni21) ni22), le_app_spec ni1 (@length nested_imp (@cons nested_imp x ni21)) *)
case ni1; clear ni1.
(* Goal: forall _ : le_ni (@nil nested_imp) (@app nested_imp (@cons nested_imp x ni21) ni22), le_app_spec (@nil nested_imp) (@length nested_imp (@cons nested_imp x ni21)) *)
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : le_ni (@cons nested_imp n l) (@app nested_imp (@cons nested_imp x ni21) ni22)), le_app_spec (@cons nested_imp n l) (@length nested_imp (@cons nested_imp x ni21)) *)
intros le; elimtype False; inversion_clear le.
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : le_ni (@cons nested_imp n l) (@app nested_imp (@cons nested_imp x ni21) ni22)), le_app_spec (@cons nested_imp n l) (@length nested_imp (@cons nested_imp x ni21)) *)
simpl in |- *; intros x' ni1 le1.
(* Goal: le_app_spec (@cons nested_imp x' ni1) (S (@length nested_imp ni21)) *)
elim (ih ni1); clear ih.
(* Goal: forall (ni11 ni12 : nested_imps) (_ : @eq nested_imps ni1 (@app nested_imp ni11 ni12)) (_ : @eq nat (@length nested_imp ni11) (@length nested_imp ni21)), le_app_spec (@cons nested_imp x' ni1) (S (@length nested_imp ni21)) *)
(* Goal: le_ni ni1 (@app nested_imp ni21 ni22) *)
intros ni11 ni12 eq len.
(* Goal: le_app_spec (@cons nested_imp x' ni1) (S (@length nested_imp ni21)) *)
(* Goal: le_ni ni1 (@app nested_imp ni21 ni22) *)
exists (x' :: ni11) ni12.
(* Goal: @Logic.eq nested_imps (@cons nested_imp x' ni1) (@app nested_imp (@cons nested_imp x' ni11) ni12) *)
(* Goal: @Logic.eq nat (@length nested_imp (@cons nested_imp x' ni11)) (S (@length nested_imp ni21)) *)
(* Goal: le_ni ni1 (@app nested_imp ni21 ni22) *)
 rewrite eq.
(* Goal: @Logic.eq nested_imps (@cons nested_imp x' (@app nested_imp ni11 ni12)) (@app nested_imp (@cons nested_imp x' ni11) ni12) *)
(* Goal: @Logic.eq nat (@length nested_imp (@cons nested_imp x' ni11)) (S (@length nested_imp ni21)) *)
(* Goal: le_ni ni1 (@app nested_imp ni21 ni22) *)
trivial.
(* Goal: @Logic.eq nat (@length nested_imp (@cons nested_imp x' ni11)) (S (@length nested_imp ni21)) *)
(* Goal: le_ni ni1 (@app nested_imp ni21 ni22) *)
simpl in |- *.
(* Goal: @Logic.eq nested_imps (@cons nested_imp x' (@app nested_imp ni11 ni12)) (@app nested_imp (@cons nested_imp x' ni11) ni12) *)
(* Goal: @Logic.eq nat (@length nested_imp (@cons nested_imp x' ni11)) (S (@length nested_imp ni21)) *)
(* Goal: le_ni ni1 (@app nested_imp ni21 ni22) *)
 rewrite len; trivial.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
inversion_clear le1; assumption.
Qed.





Lemma le_ni_app_nn :
 forall (ni1 ni2 ni3 ni4 : nested_imps) (x : nimp),
 length ni1 = length ni3 ->
 le_ni (ni1 ++ ni2) (ni3 ++ ni4) ->
 le_ni (ni1 ++ Undecorated x :: ni2) (ni3 ++ Undecorated x :: ni4).
(* Goal: forall (ni1 ni2 ni3 ni4 : nested_imps) (x : nimp) (_ : @eq nat (@length nested_imp ni1) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp ni1 (@cons nested_imp (Undecorated x) ni2)) (@app nested_imp ni3 (@cons nested_imp (Undecorated x) ni4)) *)
intros ni1 ni2 ni3 ni4 x.
(* Goal: forall (_ : @eq nat (@length nested_imp ni1) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
generalize ni3; clear ni3.
(* Goal: forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp ni1) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
elim ni1; clear ni1.
(* Goal: forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp y ni1)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp y ni1) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp y ni1) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros ni3; case ni3; clear ni3.
(* Goal: forall (_ : @eq nat (@length nested_imp (@nil nested_imp)) (@length nested_imp (@nil nested_imp))) (_ : le_ni (@app nested_imp (@nil nested_imp) ni2) (@app nested_imp (@nil nested_imp) ni4)), le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : @eq nat (@length nested_imp (@nil nested_imp)) (@length nested_imp (@cons nested_imp n l))) (_ : le_ni (@app nested_imp (@nil nested_imp) ni2) (@app nested_imp (@cons nested_imp n l) ni4)), le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp n l) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
simpl in |- *; intros len le.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Le_NI_Cons_NN; assumption.
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : @eq nat (@length nested_imp (@nil nested_imp)) (@length nested_imp (@cons nested_imp n l))) (_ : le_ni (@app nested_imp (@nil nested_imp) ni2) (@app nested_imp (@cons nested_imp n l) ni4)), le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp n l) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros y ni3 len le.
(* Goal: le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp y ni3) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
inversion_clear len.
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros y ni1 ih.
(* Goal: forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp y ni1)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp y ni1) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp y ni1) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros ni3; case ni3; clear ni3.
(* Goal: le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp y ni3) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
simpl in |- *; intros len le; inversion_clear len.
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : @eq nat (@length nested_imp (@cons nested_imp y ni1)) (@length nested_imp (@cons nested_imp n l))) (_ : le_ni (@app nested_imp (@cons nested_imp y ni1) ni2) (@app nested_imp (@cons nested_imp n l) ni4)), le_ni (@app nested_imp (@cons nested_imp y ni1) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp n l) (@cons nested_imp (Decorated x k) ni4)) *)
simpl in |- *; intros y' ni3 len le.
(* Goal: le_ni (@cons nested_imp y (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp y' (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
inversion_clear le.
(* Goal: le_ni (@cons nested_imp (Undecorated x0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Undecorated x0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Undecorated x0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
apply Le_NI_Cons_NN.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: forall (ni3 : nested_imps) (_ : eqv_ni NNil ni3), eqv_ni NNil ni3 *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
 injection len; intros; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Undecorated x0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
apply Le_NI_Cons_DN.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: forall (ni3 : nested_imps) (_ : eqv_ni NNil ni3), eqv_ni NNil ni3 *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
 injection len; intros; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
apply Le_NI_Cons_DD.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: forall (ni3 : nested_imps) (_ : eqv_ni NNil ni3), eqv_ni NNil ni3 *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
 injection len; intros; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.
Qed.



Lemma le_ni_app_dn :
 forall (ni1 ni2 ni3 ni4 : nested_imps) (x : nimp) (k : kripke_tree),
 length ni1 = length ni3 ->
 le_ni (ni1 ++ ni2) (ni3 ++ ni4) ->
 le_ni (ni1 ++ Decorated x k :: ni2) (ni3 ++ Undecorated x :: ni4).
(* Goal: forall (ni1 ni2 ni3 ni4 : nested_imps) (x : nimp) (k : kripke_tree) (_ : @eq nat (@length nested_imp ni1) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros ni1 ni2 ni3 ni4 x k.
(* Goal: forall (_ : @eq nat (@length nested_imp ni1) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
generalize ni3; clear ni3.
(* Goal: forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp ni1) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
elim ni1; clear ni1.
(* Goal: forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp y ni1)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp y ni1) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp y ni1) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros ni3; case ni3; clear ni3.
(* Goal: forall (_ : @eq nat (@length nested_imp (@nil nested_imp)) (@length nested_imp (@nil nested_imp))) (_ : le_ni (@app nested_imp (@nil nested_imp) ni2) (@app nested_imp (@nil nested_imp) ni4)), le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : @eq nat (@length nested_imp (@nil nested_imp)) (@length nested_imp (@cons nested_imp n l))) (_ : le_ni (@app nested_imp (@nil nested_imp) ni2) (@app nested_imp (@cons nested_imp n l) ni4)), le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp n l) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
simpl in |- *; intros len le.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Le_NI_Cons_DN; assumption.
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : @eq nat (@length nested_imp (@nil nested_imp)) (@length nested_imp (@cons nested_imp n l))) (_ : le_ni (@app nested_imp (@nil nested_imp) ni2) (@app nested_imp (@cons nested_imp n l) ni4)), le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp n l) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros y ni3 len le.
(* Goal: le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp y ni3) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
inversion_clear len.
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros y ni1 ih.
(* Goal: forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp y ni1)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp y ni1) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp y ni1) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros ni3; case ni3; clear ni3.
(* Goal: le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp y ni3) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
simpl in |- *; intros len le; inversion_clear len.
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : @eq nat (@length nested_imp (@cons nested_imp y ni1)) (@length nested_imp (@cons nested_imp n l))) (_ : le_ni (@app nested_imp (@cons nested_imp y ni1) ni2) (@app nested_imp (@cons nested_imp n l) ni4)), le_ni (@app nested_imp (@cons nested_imp y ni1) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp n l) (@cons nested_imp (Decorated x k) ni4)) *)
simpl in |- *; intros y' ni3 len le.
(* Goal: le_ni (@cons nested_imp y (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp y' (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
inversion_clear le.
(* Goal: le_ni (@cons nested_imp (Undecorated x0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Undecorated x0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Undecorated x0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
apply Le_NI_Cons_NN.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: forall (ni3 : nested_imps) (_ : eqv_ni NNil ni3), eqv_ni NNil ni3 *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
 injection len; intros; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Undecorated x0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
apply Le_NI_Cons_DN.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: forall (ni3 : nested_imps) (_ : eqv_ni NNil ni3), eqv_ni NNil ni3 *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
 injection len; intros; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
apply Le_NI_Cons_DD.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: forall (ni3 : nested_imps) (_ : eqv_ni NNil ni3), eqv_ni NNil ni3 *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
 injection len; intros; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.
Qed.




Lemma le_ni_app_dd :
 forall (ni1 ni2 ni3 ni4 : nested_imps) (x : nimp) (k : kripke_tree),
 length ni1 = length ni3 ->
 le_ni (ni1 ++ ni2) (ni3 ++ ni4) ->
 le_ni (ni1 ++ Decorated x k :: ni2) (ni3 ++ Decorated x k :: ni4).
(* Goal: forall (ni1 ni2 ni3 ni4 : nested_imps) (x : nimp) (k : kripke_tree) (_ : @eq nat (@length nested_imp ni1) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros ni1 ni2 ni3 ni4 x k.
(* Goal: forall (_ : @eq nat (@length nested_imp ni1) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
generalize ni3; clear ni3.
(* Goal: forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp ni1) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
elim ni1; clear ni1.
(* Goal: forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp y ni1)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp y ni1) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp y ni1) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros ni3; case ni3; clear ni3.
(* Goal: forall (_ : @eq nat (@length nested_imp (@nil nested_imp)) (@length nested_imp (@nil nested_imp))) (_ : le_ni (@app nested_imp (@nil nested_imp) ni2) (@app nested_imp (@nil nested_imp) ni4)), le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : @eq nat (@length nested_imp (@nil nested_imp)) (@length nested_imp (@cons nested_imp n l))) (_ : le_ni (@app nested_imp (@nil nested_imp) ni2) (@app nested_imp (@cons nested_imp n l) ni4)), le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp n l) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
simpl in |- *; intros len le.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
apply Le_NI_Cons_DD; assumption.
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : @eq nat (@length nested_imp (@nil nested_imp)) (@length nested_imp (@cons nested_imp n l))) (_ : le_ni (@app nested_imp (@nil nested_imp) ni2) (@app nested_imp (@cons nested_imp n l) ni4)), le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp n l) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros y ni3 len le.
(* Goal: le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp y ni3) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
inversion_clear len.
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros y ni1 ih.
(* Goal: forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp y ni1)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp y ni1) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp y ni1) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
intros ni3; case ni3; clear ni3.
(* Goal: le_ni (@app nested_imp (@nil nested_imp) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp y ni3) (@cons nested_imp (Decorated x k) ni4)) *)
(* Goal: forall (a : nested_imp) (l : list nested_imp) (_ : forall (ni3 : nested_imps) (_ : @eq nat (@length nested_imp l) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp l ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp l (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) (ni3 : nested_imps) (_ : @eq nat (@length nested_imp (@cons nested_imp a l)) (@length nested_imp ni3)) (_ : le_ni (@app nested_imp (@cons nested_imp a l) ni2) (@app nested_imp ni3 ni4)), le_ni (@app nested_imp (@cons nested_imp a l) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
simpl in |- *; intros len le; inversion_clear len.
(* Goal: forall (n : nested_imp) (l : list nested_imp) (_ : @eq nat (@length nested_imp (@cons nested_imp y ni1)) (@length nested_imp (@cons nested_imp n l))) (_ : le_ni (@app nested_imp (@cons nested_imp y ni1) ni2) (@app nested_imp (@cons nested_imp n l) ni4)), le_ni (@app nested_imp (@cons nested_imp y ni1) (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp (@cons nested_imp n l) (@cons nested_imp (Decorated x k) ni4)) *)
simpl in |- *; intros y' ni3 len le.
(* Goal: le_ni (@cons nested_imp y (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp y' (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
inversion_clear le.
(* Goal: le_ni (@cons nested_imp (Undecorated x0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Undecorated x0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Undecorated x0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
apply Le_NI_Cons_NN.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: forall (ni3 : nested_imps) (_ : eqv_ni NNil ni3), eqv_ni NNil ni3 *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
 injection len; intros; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Undecorated x0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
apply Le_NI_Cons_DN.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: forall (ni3 : nested_imps) (_ : eqv_ni NNil ni3), eqv_ni NNil ni3 *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
 injection len; intros; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.
(* Goal: le_ni (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2))) (@cons nested_imp (Decorated x0 k0) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4))) *)
apply Le_NI_Cons_DD.
(* Goal: le_ni (@app nested_imp ni1 (@cons nested_imp (Decorated x k) ni2)) (@app nested_imp ni3 (@cons nested_imp (Decorated x k) ni4)) *)
apply ih.
(* Goal: forall (ni3 : nested_imps) (_ : eqv_ni NNil ni3), eqv_ni NNil ni3 *)
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Undecorated x) ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k') ni2) ni3), eqv_ni (@cons nested_imp (Decorated x k) ni1) ni3 *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : forall (ni3 : nested_imps) (_ : eqv_ni ni2 ni3), eqv_ni ni1 ni3) (ni3 : nested_imps) (_ : eqv_ni (@cons nested_imp (Decorated x k) ni2) ni3), eqv_ni (@cons nested_imp (Undecorated x) ni1) ni3 *)
 injection len; intros; assumption.
(* Goal: le_ni (@app nested_imp ni1 ni2) (@app nested_imp ni3 ni4) *)
assumption.
Qed.



