proposition: Lemma subterm_noteq : forall u t, subterm_eq u t -> u <> t -> subterm u t.
proof: Proof. unfold subterm_eq, subterm. intros. destruct H as [C]. destruct C. subst t. simpl in H0. cong. exists (Cont e t0 C t1). split. discr. subst t. refl. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)