proposition: Lemma tc_supterm_acc_R_mon_commut : supterm_acc! @ R << R @ supterm_acc!.
proof: Proof. apply commut_tc. apply supterm_acc_R_mon_commut. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)