proposition: Lemma supterm_acc_supterm : supterm_acc << supterm!.
proof: Proof. intros t u [f ts i hi]. apply supterm_nth. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)