-ndefinition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
- #s; #s1; @ (s ⇒_1 s1); @
- [ #f; #g; napply (∀a,a':s. a=a' → f a = g a')
- | #x; #a; #a'; #Ha; napply (.= †Ha); napply refl1
- | #x; #y; #H; #a; #a'; #Ha; napply (.= †Ha); napply sym1; /2/
- | #x; #y; #z; #H1; #H2; #a; #a'; #Ha; napply (.= †Ha); napply trans1; ##[##2: napply H1 | ##skip | napply H2]//;##]
-nqed.
+definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
+ #s #s1 % [@(s ⇒_1 s1)] %
+ [ #f #g @(∀a,a':s. a=a' → f a = g a')
+ | #x #a #a' #Ha @(.= †Ha) @refl1
+ | #x #y #H #a #a' #Ha @(.= †Ha) @sym1 /2/
+ | #x #y #z #H1 #H2 #a #a' #Ha @(.= †Ha) @trans1
+ [2: @H1 | skip | @H2] // ]
+qed.