proposition: Lemma conv_env_app : forall M N (Mapp: isApp M) (Napp: isApp N) Q, conv_term (term M) (term N) Q -> conv_env (appBodyL Mapp) (appBodyL Napp) Q -> conv_env (appBodyR Mapp) (appBodyR Napp) Q -> conv_env M N Q.
proof: Proof. intros; term_inv M; term_inv N. intros p q Qpq C; unfold Tr; unfold Tr0. rewrite (activeEnv_app (buildT (TApp T1 T2)) I). rewrite (activeEnv_app (buildT (TApp T3 T4)) I). split; intro D. destruct (env_sum_varDecl (activeEnv (buildT T1)) (activeEnv (buildT T2)) D) as [[Lc Rn] | Rc]. apply env_sum_ly. apply activeEnv_app_comp. apply (proj1 (H0 p q Qpq C)); trivial. apply env_sum_ry. apply (proj1 (H1 p q Qpq C)); trivial. destruct (env_sum_varDecl (activeEnv (buildT T3)) (activeEnv (buildT T4)) D) as [[Lc Rn] | Rc]. apply env_sum_ly. apply activeEnv_app_comp. apply (proj2 (H0 p q Qpq C)); trivial. apply env_sum_ry. apply (proj2 (H1 p q Qpq C)); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)