proposition: Lemma app_conv_app_left_aux : forall M N (Mapp: isApp M) (Napp: isApp N) Q, M ~(Q) N -> (appBodyL Mapp) ~(Q) (appBodyL Napp).
proof: Proof. intros; term_inv M; term_inv N. inversion H; inversion H0. constructor; trivial. change (buildT T1) with (appBodyL (M:=buildT (TApp T1 T2)) I). change (buildT T3) with (appBodyL (M:=buildT (TApp T3 T4)) I). apply conv_env_appBodyL; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)