proposition: Lemma tc_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. revert t u tu; induction 1. apply t_step. apply supterm_acc_subs. hyp. trans (subs s y); fo. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)