proposition: Lemma subterm_wf : well_founded subterm.
proof: Proof. intros M; destruct M as [E Pt A TypM]. induction TypM; constructor; inversion 1; simpl in *; try contr. inversion H0; trivial. apply Acc_inv with (buildT TypM); trivial. inversion H0; trivial. apply Acc_inv with (buildT TypM1); trivial. inversion H0; trivial. apply Acc_inv with (buildT TypM2); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)