proposition: Lemma appHead_term : forall (M N: Term), term M = term N -> term (appHead M) = term (appHead N).
proof: Proof. intros M. apply well_founded_ind with (R := subterm) (P := fun (M: Term) => forall (N: Term), term M = term N -> term (appHead M) = term (appHead N) ). apply subterm_wf. clear M; intros M IH N M_N. term_inv M; term_inv N. unfold Tr, Tr0. rewrite !appHead_app_explicit. apply IH. constructor 1 with I; constructor 2. simpl; congruence. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)