fact: Fixpoint bsubterm_eq (t u : term) : bool := match u with | Var _ => beq_term t u | Fun _ us => beq_term t u || bVexists (bsubterm_eq t) us end.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)