proposition: Lemma notin_fv_lam x y u : y=x \/ ~In x (fv u) <-> ~In x (fv (Lam y u)).
proof: Proof. simpl. set_iff. eq_dec y x; fo. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)