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