proposition: Lemma supterm_acc_R_mon_commut : supterm_acc @ R << R @ supterm_acc.
proof: Proof. intros t v [u [tu uv]]. inversion tu; clear tu; subst. exists (apps (Fun f) (Vreplace ts (Acc_arity hi) v)). split. set (ts' := Vreplace ts (Acc_arity hi) v). rewrite <- (Vreplace_nth_eq ts (Acc_arity hi)). unfold ts'. mon. rewrite <- (Vnth_replace (Acc_arity hi) (Acc_arity hi) ts v) at 2. apply stacc_intro. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)