proposition: Lemma WF_supterm : WF supterm.
proof: Proof. intro x. apply subterm_ind. clear x. intros x IH. apply SN_intro. intros y sy. assert (subterm y x); inversion sy as [c [hole subst]]; auto. Qed.
imports: CoLoR(ATrs SN LogicUtil VecUtil VecOrd NatUtil RelUtil ARelation Union ACap ACalls) Coq(List Sumbool)