]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground_2/pull/pull_4.ma
milestone update in ground_2 and basic_2A
[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / pull / pull_4.ma
index 4bf66b56e3ea36c6982ca962c77340dc3b199d86..a2e0baffb2c5878e3da998fb9ee74ad53b247d00 100644 (file)
@@ -22,5 +22,5 @@ lemma pull_4 (A1:Type[0])
              (A4:Type[0])
              (A:∀x1:A1.∀x2:A2 x1.A3 x1 x2 → A4 → Type[0]):
              (∀x4,x1,x2,x3. A x1 x2 x3 x4) →
-             (∀x1,x2,x3,x4. A x1 x2 x3 x4). 
+             (∀x1,x2,x3,x4. A x1 x2 x3 x4).
 /2 width=1 by/ qed-.