proposition: Lemma supterm_acc_subs : forall s t u, supterm_acc t u -> supterm_acc (subs s t) (subs s u).
proof: Proof. intros s t u tu. inversion tu; clear tu; subst. rewrite subs_apps, <- Vnth_map. apply stacc_intro. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)