proposition: Lemma betaStep_type_preserving : forall M N, BetaStep M N -> type M = type N.
proof: Proof. intros. inversion H. rewrite lower_type. rewrite subst_type. destruct M as [ME MPt MT M]. destruct M; try contr. assert (MlT: type (appBodyL Mapp0) = A --> B); [simpl; trivial | idtac]. rewrite (absBody_type (appBodyL Mapp0) MLabs MlT); simpl; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)