proposition: Lemma abs_conv_absBody_aux : forall M N Q (Mabs: isAbs M) (Nabs: isAbs N), M ~(Q) N -> (absBody Mabs) ~(envSubst_lift1 Q) (absBody Nabs).
proof: Proof. intros. term_inv M; term_inv N. inversion H. constructor. inversion H0; trivial. replace (buildT T) with (@absBody (buildT (TAbs T)) I); trivial. replace (buildT T0) with (@absBody (buildT (TAbs T0)) I); trivial. apply conv_env_absBody; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)