proposition: Lemma conv_env_abs : forall M N (Mabs: isAbs M) (Nabs: isAbs N) Q, conv_term (term M) (term N) Q -> conv_env (absBody Mabs) (absBody Nabs) (envSubst_lift1 Q) -> conv_env M N Q.
proof: Proof. intros; term_inv M; term_inv N. intros p q Qpq C. unfold Tr; rewrite (activeEnv_abs (buildT (TAbs T)) I). unfold Tr0; rewrite (activeEnv_abs (buildT (TAbs T0)) I). assert (Q_pq: envSub (envSubst_lift1 Q) (S p) (S q)). destruct Q; trivial. split; intro D. apply varD_tail. apply (proj1 (H0 (S p) (S q) Q_pq C)). apply varD_tail_rev; trivial. apply varD_tail. apply (proj2 (H0 (S p) (S q) Q_pq C)). apply varD_tail_rev; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)