proposition: Lemma subterm_strict : forall u t, subterm u t -> subterm_eq u t.
proof: Proof. unfold subterm_eq, subterm. intros. destruct H. destruct H. exists x. hyp. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)