X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsyntax%2Fbind.ma;h=487722c443bad811888ee067cd145f2804e463b7;hp=ca474406d499dc2650ecdcab1aa3fc83da92e092;hb=222044da28742b24584549ba86b1805a87def070;hpb=73966e3e9fd17155ca67e6b4a32f52225cea9d3c

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma
index ca474406d..487722c44 100644
--- 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-.