proposition: Lemma subject_reduction : forall M N, M -b-> N -> type M = type N.
proof: Proof. intros. apply Red_type_preserving with BetaStep; trivial. apply betaStep_type_preserving. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)