proposition: Lemma tc_supterm_R_mon_commut : supterm! @ R << R @ supterm!.
proof: Proof. apply commut_tc. apply supterm_R_mon_commut. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)