+#Univ ##.
+#A ##.
+#B ##.
+#X ##.
+#Y ##.
+#Z ##.
+#add ##.
+#c ##.
+#d ##.
+#negate ##.
+#H0 ##.
+#H1 ##.
+#H2 ##.
+#H3 ##.
+napply (ex_intro ? ? ? ?) ##[
+##2:
+napply (ex_intro ? ? ? ?) ##[
+##2:
+nauto by H0,H1,H2,H3 ##;
+##| ##skip ##]
+##| ##skip ##]
+ntry (nassumption) ##;