we reformulate the extended computation to simplify the proof of its

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / ssta_aaa.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma
index d14083a45a1901f8b3ed2a1f500e03577ae4c346..01841483c7400ab33680a481b639d866c3eef7ab 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma
@@ -38,4 +38,3 @@ lemma ssta_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U,l. ⦃h, L⦄ ⊢ T •[g,
   lapply (ssta_inv_cast1 … H) -H /2 width=2/
 ]
 qed.
-