proposition: Lemma rename_lam_no_alpha y z x u : ~In y (fv u) \/ x=y \/ x<>z -> rename y z (Lam x u) = Lam x (subs (update x (Var x) (single y (Var z))) u).
proof: Proof. intro h. unfold Def.rename. rewrite single_lam_no_alpha. refl. simpl. set_iff. destruct h as [h|[h|h]]; auto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)