proposition: Lemma conv_env_appBodyL : forall M N (Mapp: isApp M) (Napp: isApp N) Q, conv_env M N Q -> conv_term (term M) (term N) Q -> conv_env (appBodyL Mapp) (appBodyL Napp) Q.
proof: Proof. intros. intros x y xy A. inversion H0; try solve [term_inv M; term_inv N]. assert (Ecomp: forall A B, activeEnv (appBodyL Mapp) |= x := A -> activeEnv (appBodyL Napp) |= y := B -> A = B). intros C D MC ND. assert (activeEnv N |= y := C). apply (proj1 (H x y xy C)). apply activeEnv_appBodyL_varD with Mapp; trivial. set (w := activeEnv_appBodyL_varD N Napp ND). inversion H6; inversion w; try_solve. replace LL with (term (appBodyL Mapp)) in H3. replace RL with (term (appBodyL Napp)) in H3. exact (terms_conv_var_usage (appBodyL Mapp) (appBodyL Napp) Ecomp xy H3 A). eapply appBodyL_term; eauto. eapply appBodyL_term; eauto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)