-ndefinition seteq: ∀A. equivalence_relation1 (Ω^A).
-#A; @(λS,S'. S ⊆ S' ∧ S' ⊆ S); /2/; ##[ #A B; *; /3/]
-#S T U; *; #H1 H2; *; /4/;
-nqed.
+definition seteq: ∀A. equivalence_relation1 (Ω^A).
+#A % [@(λS,S'. S ⊆ S' ∧ S' ⊆ S)]
+/2/[ #A #B * /3/]
+#S #T #U * #H1 #H2 * /4/
+qed.