proposition: Lemma size_strict_subterm : forall s t, trans_clos direct_subterm s t -> size s < size t.
proof: Proof. intros s t Sub; induction Sub as [ s t H | s u t H1 H2]. apply size_direct_subterm; assumption. apply Nat.lt_trans with (size u); trivial. apply size_direct_subterm; assumption. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)