proposition: Lemma aeq_tc_supterm_acc_commut : aeq @ (supterm_acc!) << (supterm_acc!) @ aeq.
proof: Proof. apply commut_tc_inv. apply aeq_supterm_acc_commut. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)