proposition: Lemma app_conv_app_left : forall M N (Mapp: isApp M) (Napp: isApp N), M ~ N -> terms_conv (appBodyL Mapp) (appBodyL Napp).
proof: Proof. intros; destruct H. exists x; apply app_conv_app_left_aux; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)