proposition: Lemma fv_R_notin_fv_lam : forall R x y u v, Proper (R --> Subset) fv -> R (Lam x u) (Lam y v) -> y=x \/ ~In x (fv v).
proof: Proof. intros R x y u v fv_R r. rewrite notin_fv_lam, <- r. simpl. set_iff. fo. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)