renaming in basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/item.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/item.ma
index ab861be57187a8405c5fcad6e59ff7cecf6112f2..ba835726083cffd28703c0937053c39f1e6d5d1f 100644 (file)
--- 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/