proposition: Lemma supterm_acc_wf : WF supterm_acc.
proof: Proof. eapply WF_incl. apply supterm_acc_supterm. apply WF_tc. apply supterm_wf. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)