proposition: Lemma rename1_no_alpha u x y : x=y \/ ~In x (fv u) \/ ~In y (bv u) -> rename x y u = rename1 x y u.
proof: Proof. intro h. unfold Def.rename, Def.rename1. apply subs1_no_alpha. apply inter_empty. intros z hz. rewrite fvcodom_single. case_eq (mem x (fv u) && negb (beq_term (Var y) (Var x))); simpl; set_iff. 2: fo. rewrite andb_eq, <- mem_iff, beq_term_var, negb_lr; simpl. unfold XSetFacts.eqb. eq_dec y x; split_all; subst; firstorder with bool. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)