src/ZF/Constructible/Relative.thy

      "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
 by (blast intro: univ0_downwards_mem) 
 
 text{*Congruence rule for separation: can assume the variable is in @{text M}*}
 lemma separation_cong [cong]:
-     "(!!x. M(x) ==> P(x) <-> P'(x)) ==> separation(M,P) <-> separation(M,P')"
+     "(!!x. M(x) ==> P(x) <-> P'(x)) 
+      ==> separation(M, %x. P(x)) <-> separation(M, %x. P'(x))"
 by (simp add: separation_def) 
 
 text{*Congruence rules for replacement*}
 lemma univalent_cong [cong]:
      "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
-      ==> univalent(M,A,P) <-> univalent(M,A',P')"
+      ==> univalent(M, A, %x y. P(x,y)) <-> univalent(M, A', %x y. P'(x,y))"
 by (simp add: univalent_def) 
 
 lemma strong_replacement_cong [cong]:
      "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
-      ==> strong_replacement(M,P) <-> strong_replacement(M,P')" 
+      ==> strong_replacement(M, %x y. P(x,y)) <-> 
+          strong_replacement(M, %x y. P'(x,y))" 
 by (simp add: strong_replacement_def) 
 
 text{*The extensionality axiom*}
 lemma "extensionality(\<lambda>x. x \<in> univ(0))"
 apply (simp add: extensionality_def)

      "[| X \<in> univ(A);  Transset(A) |] ==> Collect(X,P) \<in> univ(A)"
 by (simp add: univ_def Collect_in_VLimit Limit_nat)
 
 lemma "separation(\<lambda>x. x \<in> univ(0), P)"
 apply (simp add: separation_def, clarify) 
-apply (rule_tac x = "Collect(x,P)" in bexI) 
+apply (rule_tac x = "Collect(z,P)" in bexI) 
 apply (blast intro: Collect_in_univ Transset_0)+
 done
 
 text{*Unordered pairing axiom*}
 lemma "upair_ax(\<lambda>x. x \<in> univ(0))"