proposition: Lemma subs_lam_no_alpha s x u : ~In x (fvcodom (remove x (fv u)) s) -> subs s (Lam x u) = Lam x (subs (update x (Var x) s) u).
proof: Proof. rewrite not_mem_iff. intro n. simpl. unfold Def.var; ens. rewrite n. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)