regenerated

[helm.git] / helm / software / matita / contribs / TPTP / HEQ / LCL151-1.ma

diff --git a/helm/software/matita/contribs/TPTP/HEQ/LCL151-1.ma b/helm/software/matita/contribs/TPTP/HEQ/LCL151-1.ma
index 6403141f27614d11087fc5726c0a47569601fcff..e22f7a7683e21177ff087c147b9a9b4f7560e434 100644 (file)
--- a/helm/software/matita/contribs/TPTP/HEQ/LCL151-1.ma
+++ b/helm/software/matita/contribs/TPTP/HEQ/LCL151-1.ma
@@ -145,7 +145,7 @@ include "logic/equality.ma".
 
 (* -------------------------------------------------------------------------- *)
 theorem prove_wajsberg_theorem:
- ∀Univ:Set.∀X:Univ.∀Y:Univ.∀Z:Univ.∀big_V:∀_:Univ.∀_:Univ.Univ.∀big_hat:∀_:Univ.∀_:Univ.Univ.∀implies:∀_:Univ.∀_:Univ.Univ.∀not:∀_:Univ.Univ.∀ordered:∀_:Univ.∀_:Univ.Prop.∀truth:Univ.∀x:Univ.∀y:Univ.∀z:Univ.∀H0:∀X:Univ.∀Y:Univ.∀_:eq Univ (implies X Y) truth.ordered X Y.∀H1:∀X:Univ.∀Y:Univ.∀_:ordered X Y.eq Univ (implies X Y) truth.∀H2:∀X:Univ.∀Y:Univ.eq Univ (big_hat X Y) (not (big_V (not X) (not Y))).∀H3:∀X:Univ.∀Y:Univ.eq Univ (big_V X Y) (implies (implies X Y) Y).∀H4:∀X:Univ.∀Y:Univ.eq Univ (implies (implies (not X) (not Y)) (implies Y X)) truth.∀H5:∀X:Univ.∀Y:Univ.eq Univ (implies (implies X Y) Y) (implies (implies Y X) X).∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (implies (implies X Y) (implies (implies Y Z) (implies X Z))) truth.∀H7:∀X:Univ.eq Univ (implies truth X) X.eq Univ (big_V (big_hat x y) z) (big_hat (big_V x z) (big_V y z))
+ ∀Univ:Set.∀X:Univ.∀Y:Univ.∀Z:Univ.∀big_V:∀_:Univ.∀_:Univ.Univ.∀big_hat:∀_:Univ.∀_:Univ.Univ.∀implies:∀_:Univ.∀_:Univ.Univ.∀not:∀_:Univ.Univ.∀ordered:∀_:Univ.∀_:Univ.Prop.∀truth:Univ.∀x:Univ.∀y:Univ.∀z:Univ.∀H0:∀X:Univ.∀Y:Univ.∀_:ordered X Y.eq Univ (implies X Y) truth.∀H1:∀X:Univ.∀Y:Univ.∀_:ordered X Y.eq Univ (implies X Y) truth.∀H2:∀X:Univ.∀Y:Univ.eq Univ (big_hat X Y) (not (big_V (not X) (not Y))).∀H3:∀X:Univ.∀Y:Univ.eq Univ (big_V X Y) (implies (implies X Y) Y).∀H4:∀X:Univ.∀Y:Univ.eq Univ (implies (implies (not X) (not Y)) (implies Y X)) truth.∀H5:∀X:Univ.∀Y:Univ.eq Univ (implies (implies X Y) Y) (implies (implies Y X) X).∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (implies (implies X Y) (implies (implies Y Z) (implies X Z))) truth.∀H7:∀X:Univ.eq Univ (implies truth X) X.eq Univ (big_V (big_hat x y) z) (big_hat (big_V x z) (big_V y z))
 .
 intros.
 autobatch paramodulation timeout=600;