proposition: Lemma subterm_ind : forall (P : term -> Prop) (IH : forall t, (forall u, subterm u t -> P u) -> P t), forall t, P t.
proof: Proof. intros. apply subterm_eq_rect. apply subterm_sub_ind. hyp. Qed.
imports: CoLoR(LogicUtil) CoLoR(ListUtil)