#s; #s1; @ (unary_morphism1 s s1); @
[ #f; #g; napply (∀a:s. f a = g a)
| #x; #a; napply refl1
- | #x; #y; #H; #a; napply sym1; nauto
+ | #x; #y; #H; #a; napply sym1; //
| #x; #y; #z; #H1; #H2; #a; napply trans1; ##[##2: napply H1 | ##skip | napply H2]##]
nqed.