some restyling ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_conversion / lpce.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce.ma
index b74313dae70a5bf42891f4404498663ad833fe0a..8da6c1af49c1378e4bb34e543aff6651b478f5b9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce.ma
@@ -62,7 +62,7 @@ lemma lpce_inv_bind_dx (h) (G):
 
 lemma lpce_inv_unit_sn (h) (G):
       ∀I,L2,K1. ⦃G,K1.ⓤ{I}⦄ ⊢ ⬌η[h] L2 →
-      ∃∃K2. ⦃G, K1⦄ ⊢ ⬌η[h] K2 & L2 = K2.ⓤ{I}.
+      ∃∃K2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & L2 = K2.ⓤ{I}.
 /2 width=1 by lex_inv_unit_sn/ qed-.
 
 lemma lpce_inv_pair_sn (h) (G):