X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Flenv.ma;h=8de779e7759706bb39781a06aa36430198cd75e3;hp=7e2b65da522b57cfa0f01646a263be6ae79c23cb;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lenv.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lenv.ma
index 7e2b65da5..8de779e77 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/lenv.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lenv.ma
@@ -70,13 +70,13 @@ lemma cfull_dec: ∀L,T1,T2. Decidable (cfull L T1 T2).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact destruct_lbind_lbind_aux: ∀I1,I2,L1,L2. L1.ⓘ{I1} = L2.ⓘ{I2} →
+fact destruct_lbind_lbind_aux: ∀I1,I2,L1,L2. L1.ⓘ[I1] = L2.ⓘ[I2] →
                                L1 = L2 ∧ I1 = I2.
 #I1 #I2 #L1 #L2 #H destruct /2 width=1 by conj/
 qed-.
 
 (* Basic_2A1: uses: discr_lpair_x_xy *)
-lemma discr_lbind_x_xy: ∀I,L. L = L.ⓘ{I} → ⊥.
+lemma discr_lbind_x_xy: ∀I,L. L = L.ⓘ[I] → ⊥.
 #I #L elim L -L
 [ #H destruct
 | #L #J #IHL #H elim (destruct_lbind_lbind_aux … H) -H  (**) (* destruct lemma needed *)
@@ -85,5 +85,5 @@ lemma discr_lbind_x_xy: ∀I,L. L = L.ⓘ{I} → ⊥.
 qed-.
 
 (* Basic_2A1: uses: discr_lpair_xy_x *)
-lemma discr_lbind_xy_x: ∀I,L. L.ⓘ{I} = L → ⊥.
+lemma discr_lbind_xy_x: ∀I,L. L.ⓘ[I] = L → ⊥.
 /2 width=4 by discr_lbind_x_xy/ qed-.