update in ground_2 and basic_2 ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lpxs_aaa.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma
index 80c43c731c5b0a4347544ee8ee9ee574a3e51c44..89122eb557cfa4447b1629e33272662c5432ef56 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma
@@ -27,6 +27,4 @@ qed-.
 
 lemma aaa_lprs_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
                      ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-#G #L1 #T #A #HT #L2 #HL12
-@(aaa_lpxs_conf … HT) -A -T /2 width=3/
-qed-.
+/3 width=5 by lprs_lpxs, aaa_lpxs_conf/ qed-.