proposition: Lemma conv_env_appBodyR : forall M N (Mapp: isApp M) (Napp: isApp N) Q, conv_env M N Q -> conv_term (term M) (term N) Q -> conv_env (appBodyR Mapp) (appBodyR 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 (appBodyR Mapp) |= x := A -> activeEnv (appBodyR Napp) |= y := B -> A = B). intros C D MC ND. assert (activeEnv N |= y := C). apply (proj1 (H x y xy C)). apply activeEnv_appBodyR_varD with Mapp; trivial. set (w := activeEnv_appBodyR_varD N Napp ND). inversion H6; inversion w; try_solve. replace LR with (term (appBodyR Mapp)) in H4. replace RR with (term (appBodyR Napp)) in H4. exact (terms_conv_var_usage (appBodyR Mapp) (appBodyR Napp) Ecomp xy H4 A). eapply appBodyR_term; eauto. eapply appBodyR_term; eauto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)