proposition: Lemma app_beta_isapp : forall M N f, M -b-> N -> term (appHead M) = ^f -> isApp N.
proof: Proof. intro M; term_inv M. intros; exfalso. apply beta_notFunS with Tr N; trivial. unfold Tr; auto with terms. intros N f MbN Mhead. inversion MbN; try solve [contr | trivial]. exfalso. inversion H. apply beta_direct_funApp with Tr I; eauto with terms. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)