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