(* Basic properties *********************************************************)
lemma eq_item0_dec: ∀I1,I2:item0. Decidable (I1 = I2).
* #i1 * #i2 [2,3,4,6,7,8: @or_intror #H destruct ]
(* Basic properties *********************************************************)
lemma eq_item0_dec: ∀I1,I2:item0. Decidable (I1 = I2).
* #i1 * #i2 [2,3,4,6,7,8: @or_intror #H destruct ]