regenerated

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

diff --git a/helm/software/matita/contribs/TPTP/HEQ/LDA004-1.ma b/helm/software/matita/contribs/TPTP/HEQ/LDA004-1.ma
index 81c0b723be2b325d1093cb39e0e96c48e6ca44da..80400ad8ff28b09a302280bbccb06889125549d7 100644 (file)
--- a/helm/software/matita/contribs/TPTP/HEQ/LDA004-1.ma
+++ b/helm/software/matita/contribs/TPTP/HEQ/LDA004-1.ma
@@ -51,7 +51,7 @@ include "logic/equality.ma".
 
 (* ----3*2*U2 is a left segment of U1*U3  *)
 theorem prove_equation:
- ∀Univ:Set.∀X:Univ.∀Y:Univ.∀Z:Univ.∀a:Univ.∀b:Univ.∀f:∀_:Univ.∀_:Univ.Univ.∀left:∀_:Univ.∀_:Univ.Prop.∀n1:Univ.∀n2:Univ.∀n3:Univ.∀u:Univ.∀u1:Univ.∀u2:Univ.∀u3:Univ.∀H0:eq Univ b (f u1 u3).∀H1:eq Univ a (f (f n3 n2) u2).∀H2:eq Univ u3 (f u n3).∀H3:eq Univ u2 (f u n2).∀H4:eq Univ u1 (f u n1).∀H5:eq Univ u (f n2 n2).∀H6:eq Univ n3 (f n2 n1).∀H7:eq Univ n2 (f n1 n1).∀H8:∀X:Univ.∀Y:Univ.∀Z:Univ.∀_:left X Y.∀_:left Y Z.left X Z.∀H9:∀X:Univ.∀Y:Univ.left X (f X Y).∀H10:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (f X (f Y Z)) (f (f X Y) (f X Z)).left a b
+ ∀Univ:Set.∀X:Univ.∀Y:Univ.∀Z:Univ.∀a:Univ.∀b:Univ.∀f:∀_:Univ.∀_:Univ.Univ.∀left:∀_:Univ.∀_:Univ.Prop.∀n1:Univ.∀n2:Univ.∀n3:Univ.∀u:Univ.∀u1:Univ.∀u2:Univ.∀u3:Univ.∀H0:eq Univ b (f u1 u3).∀H1:eq Univ a (f (f n3 n2) u2).∀H2:eq Univ u3 (f u n3).∀H3:eq Univ u2 (f u n2).∀H4:eq Univ u1 (f u n1).∀H5:eq Univ u (f n2 n2).∀H6:eq Univ n3 (f n2 n1).∀H7:eq Univ n2 (f n1 n1).∀H8:∀X:Univ.∀Y:Univ.∀Z:Univ.∀_:left Y Z.∀_:left X Y.left X Z.∀H9:∀X:Univ.∀Y:Univ.left X (f X Y).∀H10:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (f X (f Y Z)) (f (f X Y) (f X Z)).left a b
 .
 intros.
 autobatch depth=5 width=5 size=20 timeout=10;