proposition: Lemma appHead_app_explicit : forall E PtL PtR A B (L: E |- PtL := A --> B) (R: E |- PtR := A), appHead (buildT (TApp L R)) = appHead (buildT L).
proof: Proof. intros. rewrite (appHead_app (buildT (TApp L R)) I). trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)