X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fpull%2Fpull_4.ma;h=a2e0baffb2c5878e3da998fb9ee74ad53b247d00;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=4bf66b56e3ea36c6982ca962c77340dc3b199d86;hpb=05b047be6817f430c8c72fd9b0902df8bb9f579e;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground_2/pull/pull_4.ma b/matita/matita/contribs/lambdadelta/ground_2/pull/pull_4.ma index 4bf66b56e..a2e0baffb 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/pull/pull_4.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/pull/pull_4.ma @@ -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-.