-ndefinition unary_morph_setoid : setoid → setoid → setoid.
-#S1; #S2; @ (S1 ⇒_0 S2); @;
-##[ #f; #g; napply (∀x,x'. x=x' → f x = g x');
-##| #f; #x; #x'; #Hx; napply (.= †Hx); napply #;
-##| #f; #g; #H; #x; #x'; #Hx; napply ((H … Hx^-1)^-1);
-##| #f; #g; #h; #H1; #H2; #x; #x'; #Hx; napply (trans … (H1 …) (H2 …)); //; ##]
-nqed.
+definition unary_morph_setoid : setoid → setoid → setoid.
+#S1 #S2 @(mk_setoid … (S1 ⇒_0 S2)) %
+[ #f #g @(∀x,x'. x=x' → f x = g x')
+| #f #x #x' #Hx @(.= †Hx) @#
+| #f #g #H #x #x' #Hx @((H … Hx^-1)^-1)
+| #f #g #h #H1 #H2 #x #x' #Hx @(trans … (H1 …) (H2 …)) // ]
+qed.