proposition: Lemma conv_term_comp_refl : forall M N (MN: env M [<->] env N), term M = term N -> conv_term (term M) (term N) (compEnvSubst MN).
proof: Proof. intro M; destruct M as [EM PtM TM M]. induction M; intros N MN MN_term; rewrite <- MN_term; simpl. term_inv N. constructor 1; repeat split. exists A; trivial. exists A0; inversion MN_term; trivial. constructor 2. constructor 3. replace (@compEnvSubst E (env N) MN) with (@compEnvSubst (env (buildT (TAbs M))) (env N) MN); trivial. destruct N as [??? typingN]; destruct typingN; inversion MN_term. assert (EE0: decl A E [<->] decl A0 E0). unfold decl; apply env_comp_cons; trivial. left; try_solve. rewrite (envSubst_eq_abs (buildT (TAbs M)) (buildT (TAbs typingN)) I I MN EE0). set (w := IHM (buildT typingN) EE0); simpl in w. rewrite <- H1 in w. apply w; trivial. constructor 4; term_inv N; inversion MN_term. set (w := IHM1 (appBodyL (M:=buildT (TApp T1 T2)) I)). rewrite H0 in w; apply w; trivial. set (w := IHM2 (appBodyR (M:=buildT (TApp T1 T2)) I)). rewrite H1 in w; apply w; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)