proposition: Lemma abs_conv_absType : forall M N (Mabs: isAbs M) (Nabs: isAbs N), M ~ N -> absType Mabs = absType Nabs.
proof: Proof. intros M N; term_inv M; term_inv N; intros. destruct H; destruct H; inversion H; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)