proposition: Lemma conv_env_ext : forall M N Q Q', conv_term (term M) (term N) Q -> conv_env M N Q -> Q' |=> Q -> conv_env M N Q'.
proof: Proof. destruct M as [E Pt T M]; induction M; intros N Q Q' MN_term MN_env Q'Q; term_inv N; inversion MN_term; intros p q Q'pq C. split; intro D. destruct (@activeEnv_var_det (buildT (TVar v)) x p C); trivial. assert (q = x0). apply (envSub_Lok Q' x q x0). rewrite <- H3; trivial. apply Q'Q; trivial. rewrite H5. apply (proj1 (MN_env x x0 H1 C)). rewrite H4. apply activeEnv_var_decl; trivial. destruct (@activeEnv_var_det (buildT (TVar T)) x0 q C); trivial. assert (p = x). apply (envSub_Rok Q' p x x0). rewrite <- H3; trivial. apply Q'Q; trivial. rewrite H5. apply (proj2 (MN_env x x0 H1 C)). rewrite H4. apply activeEnv_var_decl; trivial. simpl; split; intros D; destruct p; destruct q; try_solve. assert (Env_conv: conv_env (buildT (TAbs M)) (buildT (TAbs T)) Q'). apply conv_env_abs with I I; trivial. apply conv_term_ext with Q; trivial. apply IHM with (envSubst_lift1 Q); trivial. apply (conv_env_absBody (M:=buildT (TAbs M)) (N:=buildT (TAbs T)) I I); trivial. apply envSubst_lift1_ext; trivial. apply (Env_conv p q Q'pq). set (envL_conv := @conv_env_appBodyL (buildT (TApp M1 M2)) (buildT (TApp T1 T2)) I I Q MN_env MN_term). set (IHL := IHM1 (buildT T1) Q Q' H4 envL_conv Q'Q). set (envR_conv := @conv_env_appBodyR (buildT (TApp M1 M2)) (buildT (TApp T1 T2)) I I Q MN_env MN_term). set (IHR := IHM2 (buildT T2) Q Q' H5 envR_conv Q'Q). set (MNQ'_term := conv_term_ext MN_term Q'Q). apply (conv_env_app (buildT (TApp M1 M2)) (buildT (TApp T1 T2)) I I MNQ'_term IHL IHR p q Q'pq). Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)