renaming in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / syntax / bind.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma
index ca474406d499dc2650ecdcab1aa3fc83da92e092..487722c443bad811888ee067cd145f2804e463b7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma
@@ -25,12 +25,10 @@ inductive bind: Type[0] ≝
 
 lemma eq_bind_dec: ∀I1,I2:bind. Decidable (I1 = I2).
 * #I1 [2: #V1 ] * #I2 [2,4: #V2 ]
-[ elim (eq_bind2_dec I1 I2) #HI
-  [ elim (eq_term_dec V1 V2) #HV /2 width=1 by or_introl/ ]
-  @or_intror #H destruct /2 width=1 by/
-| @or_intror #H destruct
-| @or_intror #H destruct
-| elim (eq_bind1_dec I1 I2) #HI /2 width=1 by or_introl/
-  @or_intror #H destruct /2 width=1 by/
+[1: elim (eq_bind2_dec I1 I2) #HI
+    [ elim (eq_term_dec V1 V2) #HV ]
+|4: elim (eq_bind1_dec I1 I2) #HI
 ]
+/2 width=1 by or_introl/
+@or_intror #H destruct /2 width=1 by/
 qed-.