proposition: Lemma supterm_acc_size : supterm_acc << transp (ltof size).
proof: Proof. intros t u tu. apply size_subpterm_acc. hyp. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)