proposition: Lemma clos_aeq_supterm_acc_R_mon_commut : clos_aeq supterm_acc @ R << R @ clos_aeq supterm_acc.
proof: Proof. intros t v [u [tu uv]]. inversion tu; clear tu; subst; rename u' into t'; rename v' into u'. assert (a : (supterm_acc @ R) t' v). exists u'. rewrite H0 in uv. fo. destruct (supterm_acc_R_mon_commut R_mon a) as [w [t'w wv]]. exists w. split. rewrite H. hyp. apply clos_aeq_intro_refl. hyp. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)