proposition: Lemma terms_conv_eq_type : forall M N, M ~ N -> type M = type N.
proof: Proof. destruct M as [EM PtM AM M]. induction M; intros; inversion H; inversion H0; inversion H1; destruct N as [EN PtN AN N]; destruct N; try_solve. assert (env (buildT (TVar v0)) |= x2 := A). apply activeEnv_subset. inversion H4. rewrite H8 in H5. apply (proj1 (H2 x x2 H5 A)). apply activeEnv_var_decl; trivial. inversion H7; inversion v0; try_solve. rewrite (IHM (buildT N)); try_solve. inversion H1; exists (envSubst_lift1 x); constructor; trivial. replace (buildT M) with (absBody (M := buildT (TAbs M)) I); trivial. replace (buildT N) with (absBody (M := buildT (TAbs N)) I); trivial. apply conv_env_absBody; trivial. inversion H5. assert (M1N1: terms_conv (buildT M1) (buildT N1)). exists x; constructor; simpl; trivial. inversion H5; rewrite <- H10; trivial. replace (buildT M1) with (appBodyL (M := buildT (TApp M1 M2)) I); trivial. replace (buildT N1) with (appBodyL (M := buildT (TApp N1 N2)) I); trivial. apply conv_env_appBodyL; trivial. set (w := IHM1 (buildT N1) M1N1); try_solve. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)