proposition: Lemma envSubst_eq_cons : forall S1 S2, envSubst_lower S1 <=> envSubst_lower S2 -> envSub S1 0 0 -> envSub S2 0 0 -> S1 <=> S2.
proof: Proof. intros S1 S2 S1S2 S10 S20; constructor; intros i j ij; destruct S1; destruct S2. destruct i; destruct j. auto. set (hint := envSub_Lok1 0 0 (S j)); fo; try_solve. set (hint := envSub_Rok1 0 (S i) 0); fo; try_solve. fo. destruct i; destruct j. fo. set (hint := envSub_Lok0 0 0 (S j)); fo; try_solve. set (hint := envSub_Rok0 0 (S i) 0); fo; try_solve. fo. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)