proposition: Lemma rename_lam x y z u : rename x y (Lam z u) = if mem x (fv u) && negb (eqb y x) && eqb y z then let z' := var_notin (add y (fv u)) in Lam z' (subs (update z (Var z') (single x (Var y))) u) else if eqb z x then Lam z u else Lam z (rename x y u).
proof: Proof. unfold Def.rename at 1. simpl. rewrite var_single, beq_term_var. simpl. rewrite singleton_b. case_eq (mem x (fv u) && negb (eqb z x) && negb (eqb y x) && eqb y z). rewrite !andb_true_iff. intros [[[h1 h2] h3] h4]. rewrite h1, h3, h4. simpl. assert (e : var_notin (union (fv u) (singleton y)) = var_notin (add y (fv u))). apply var_notin_e. rewrite union_sym, <- add_union_singleton. refl. rewrite e. refl. rewrite !andb_false_iff. intros [[[h|h]|h]|h]. rewrite h. simpl. eq_dec z x. subst z. rewrite update_single_eq, single_id. refl. rewrite update_id_single. 2: auto. refl. revert h. rewrite negb_false_iff, eqb_true_iff. intro h. subst z. rewrite update_single_eq, single_id. rewrite <- andb_assoc. rewrite andb_comm with (b2:=eqb y x), andb_negb_r, andb_false_r, eqb_refl. refl. rewrite h. rewrite andb_false_r. simpl. eq_dec z x. subst z. rewrite update_single_eq, single_id. refl. rewrite update_id_single. 2: auto. revert h. rewrite negb_false_iff, eqb_true_iff. intro h. subst y. rewrite single_id, rename_id. refl. rewrite h. rewrite !andb_false_r. eq_dec z x. subst z. rewrite update_single_eq, single_id. refl. rewrite update_id_single. 2: auto. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)