proposition: Lemma abs_conv_absBody : forall M N (Mabs: isAbs M) (Nabs: isAbs N), M ~ N -> terms_conv (absBody Mabs) (absBody Nabs).
proof: Proof. intros; inversion H. exists (envSubst_lift1 x). apply abs_conv_absBody_aux; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)