proposition: Lemma clos_aeq_supterm_acc_wf : WF (clos_aeq supterm_acc).
proof: Proof. apply clos_aeq_wf_size. apply supterm_acc_size. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)