proposition: Lemma forall_subterm_eq : forall (P : term -> Prop) t, (forall u, subterm_eq u t -> P u) -> P t.
proof: Proof. intros. apply H. unfold subterm. exists Hole. auto. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)