proposition: Lemma subterm_eq_split : forall t u, subterm_eq t u -> t = u \/ subterm t u.
proof: Proof. intros t u tu. destruct tu as [c hu]. destruct c. auto. right. exists (Cont e t0 c t1). intuition. discr. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)