proposition: Lemma beta_type: forall M (Mapp: isApp M) (MLabs: isAbs (appBodyL Mapp)), absType MLabs = type (appBodyR Mapp).
proof: Proof. intros. destruct M as [??? typingM]. destruct typingM; try contr. assert (type (appBodyL Mapp) = A --> B). trivial. rewrite (abs_type (appBodyL Mapp) MLabs H); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)