fact: Fixpoint bv (t : Te) := match t with | Var _ => empty | Fun _ => empty | App u v => union (bv u) (bv v) | Lam x u => add x (bv u) end.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)