proposition: Lemma transpose_rename x y : forall u, ~In y (fv u) -> ~In y (bv u) -> transpose x y u ~~ rename x y u.
proof: Proof. unfold Def.transpose. induction u; simpl; set_iff; intros h1 h2; unfold Def.rename. unfold Def.transpose_var, Def.single, Def.update; simpl. eq_dec x0 x. refl. eq_dec x0 y. subst. cong. refl. refl. rewrite IHu1; [idtac|fo|fo]. rewrite IHu2; [idtac|fo|fo]. refl. rewrite IHu; [idtac|fo|fo]. rewrite subs_lam_no_alpha. 2:{ rewrite fvcodom_single. destruct (mem x (remove x0 (fv u)) && negb (beq_term (Var y) (Var x))). simpl. set_iff. fo. set_iff. fo. } unfold Def.transpose_var. eq_dec x0 x. subst. rewrite <- aeq_alpha. 2: fo. rewrite update_single_eq, single_id. refl. eq_dec x0 y. fo. rewrite update_id_single. 2: fo. refl. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)