-#Univ.
-#X.
-#Y.
-#Z.
-#apply.
-#b.
-#combinator.
-#i.
-#k.
-#s.
-#x.
-#H0.
-#H1.
-#H2.
-#H3.
-#H4.
-napply ex_intro[
-nid2:
-nauto by H0,H1,H2,H3,H4;
-nid|
-skip]
+#Univ ##.
+#X ##.
+#Y ##.
+#Z ##.
+#apply ##.
+#b ##.
+#combinator ##.
+#i ##.
+#k ##.
+#s ##.
+#x ##.
+#H0 ##.
+#H1 ##.
+#H2 ##.
+#H3 ##.
+#H4 ##.
+napply (ex_intro ? ? ? ?) ##[
+##2:
+nauto by H0,H1,H2,H3,H4 ##;
+##| ##skip ##]
+ntry (nassumption) ##;