proposition: Lemma single_lam_no_alpha y v x u : ~In y (fv u) \/ x=y \/ v=Var y \/ ~In x (fv v) -> subs (single y v) (Lam x u) = Lam x (subs (update x (Var x) (single y v)) u).
proof: Proof. rewrite !not_mem_iff, <- eqb_true_iff, <- beq_term_true_iff, <- !negb_false_iff. simpl. rewrite var_single. intros [h|[h|[h|h]]]; rewrite h; repeat rewrite !andb_false_r; refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)