proposition: Lemma aeq_supterm_acc_commut : aeq @ supterm_acc << supterm_acc @ aeq.
proof: Proof. intros t u [t' [tt' t'u]]. inversion t'u; clear t'u; subst. inv_aeq tt'; subst. exists (Vnth us (Acc_arity hi)). split. apply stacc_intro. apply Vforall2_elim_nth. hyp. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)