(* -------------------------------------------------------------------------- *)
ntheorem prove_strong_fixed_point:
- ∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
+ (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
∀apply:∀_:Univ.∀_:Univ.Univ.
∀fixed_pt:Univ.
∀k:Univ.
∀strong_fixed_point:Univ.
∀H0:eq Univ strong_fixed_point (apply (apply s (apply k (apply (apply s (apply (apply s k) k)) (apply (apply s k) k)))) (apply (apply s (apply (apply s (apply k s)) k)) (apply k (apply (apply s (apply (apply s k) k)) (apply (apply s k) k))))).
∀H1:∀X:Univ.∀Y:Univ.eq Univ (apply (apply k X) Y) X.
-∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply s X) Y) Z) (apply (apply X Z) (apply Y Z)).eq Univ (apply strong_fixed_point fixed_pt) (apply fixed_pt (apply strong_fixed_point fixed_pt))
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply s X) Y) Z) (apply (apply X Z) (apply Y Z)).eq Univ (apply strong_fixed_point fixed_pt) (apply fixed_pt (apply strong_fixed_point fixed_pt)))
.
-#Univ.
-#X.
-#Y.
-#Z.
-#apply.
-#fixed_pt.
-#k.
-#s.
-#strong_fixed_point.
-#H0.
-#H1.
-#H2.
-nauto by H0,H1,H2;
+#Univ ##.
+#X ##.
+#Y ##.
+#Z ##.
+#apply ##.
+#fixed_pt ##.
+#k ##.
+#s ##.
+#strong_fixed_point ##.
+#H0 ##.
+#H1 ##.
+#H2 ##.
+nauto by H0,H1,H2 ##;
nqed.
(* -------------------------------------------------------------------------- *)