proposition: Lemma abs_conv : forall M N (Mabs: isAbs M) (Nabs: isAbs N) Q, absType Mabs = absType Nabs -> (absBody Mabs) ~(envSubst_lift1 Q) (absBody Nabs) -> M ~(Q) N.
proof: Proof. intros. term_inv M; term_inv N. assert (Conv_term: conv_term (\A => Pt) (\A0 => Pt0) Q). simpl; rewrite H. constructor 3. destruct H0; trivial. constructor; trivial. apply conv_env_abs with I I; simpl; trivial. destruct H0; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)