proposition: Lemma app_beta_headSymbol : forall M N f, M -b-> N -> term (appHead M) = ^f -> term (appHead N) = ^f.
proof: Proof. destruct M as [E Pt T TypM]. induction TypM; simpl; intros N f' Nbeta Mhead; try discr; inversion Nbeta; try contr. inversion H; contr. inversion H. exfalso. apply beta_direct_funApp with (buildT (TApp TypM1 TypM2)) Mapp0; eauto with terms. term_inv N. unfold Tr. rewrite appHead_app_explicit. apply IHTypM1 with (N := @appBodyL (buildT (TApp T1 T2)) I). simpl; trivial. rewrite appHead_app_explicit in Mhead; trivial. term_inv N. rewrite <- Mhead. unfold Tr. rewrite !appHead_app_explicit. congruence. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)