X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsyntax%2Fitem.ma;h=ba835726083cffd28703c0937053c39f1e6d5d1f;hp=ab861be57187a8405c5fcad6e59ff7cecf6112f2;hb=222044da28742b24584549ba86b1805a87def070;hpb=09b4420070d6a71990e16211e499b51dbb0742cb

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/item.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/item.ma
index ab861be57..ba8357260 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/item.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/item.ma
@@ -24,6 +24,11 @@ inductive item0: Type[0] ≝
    | GRef: nat → item0 (* reference by position: starting at 0 *)
 .
 
+(* unary binding items *)
+inductive bind1: Type[0] ≝
+  | Void: bind1 (* exclusion *)
+.
+
 (* binary binding items *)
 inductive bind2: Type[0] ≝
   | Abbr: bind2 (* abbreviation *)
@@ -56,6 +61,10 @@ lemma eq_item0_dec: ∀I1,I2:item0. Decidable (I1 = I2).
 #Hni12 @or_intror #H destruct /2 width=1 by/
 qed-.
 
+lemma eq_bind1_dec: ∀I1,I2:bind1. Decidable (I1 = I2).
+* * /2 width=1 by or_introl/
+qed-.
+
 (* Basic_1: was: bind_dec *)
 lemma eq_bind2_dec: ∀I1,I2:bind2. Decidable (I1 = I2).
 * * /2 width=1 by or_introl/