+
+nlemma decidable_strid_aux1 : ∀s1,n1,s2,n2.s1 ≠ s2 → (mk_strId s1 n1) ≠ (mk_strId s2 n2).
+ #s1; #n1; #s2; #n2;
+ nnormalize; #H; #H1;
+ napply (H (strid_destruct_1 … H1)).
+nqed.
+
+nlemma decidable_strid_aux2 : ∀s1,n1,s2,n2.n1 ≠ n2 → (mk_strId s1 n1) ≠ (mk_strId s2 n2).
+ #s1; #n1; #s2; #n2;
+ nnormalize; #H; #H1;
+ napply (H (strid_destruct_2 … H1)).
+nqed.
+
+nlemma decidable_strid : ∀x,y:strId.decidable (x = y).
+ #x; nelim x; #s1; #n1;
+ #y; nelim y; #s2; #n2;
+ nnormalize;
+ napply (or2_elim (s1 = s2) (s1 ≠ s2) ? (decidable_str s1 s2) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_strid_aux1 … H))
+ ##| ##1: #H; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2) …);
+ ##[ ##2: #H1; napply (or2_intro2 … (decidable_strid_aux2 … H1))
+ ##| ##1: #H1; nrewrite > H; nrewrite > H1;
+ napply (or2_intro1 … (refl_eq ? (mk_strId s2 n2)))
+ ##]
+ ##]
+nqed.
+
+nlemma neqstrid_to_neq : ∀sid1,sid2:strId.(eq_strId sid1 sid2 = false) → (sid1 ≠ sid2).
+ #sid1; nelim sid1; #s1; #n1;
+ #sid2; nelim sid2; #s2; #n2;
+ nchange with ((((eq_str s1 s2) ⊗ (eq_nat n1 n2)) = false) → ?);
+ #H;
+ napply (or2_elim ((eq_str s1 s2) = false) ((eq_nat n1 n2) = false) ? (andb_false2 … H) …);
+ ##[ ##1: #H1; napply (decidable_strid_aux1 … (neqstr_to_neq … H1))
+ ##| ##2: #H1; napply (decidable_strid_aux2 … (neqnat_to_neq … H1))
+ ##]
+nqed.
+
+nlemma strid_destruct : ∀s1,s2,n1,n2.(mk_strId s1 n1) ≠ (mk_strId s2 n2) → s1 ≠ s2 ∨ n1 ≠ n2.
+ #s1; #s2; #n1; #n2;
+ nnormalize; #H;
+ napply (or2_elim (s1 = s2) (s1 ≠ s2) ? (decidable_str s1 s2) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2) …);
+ ##[ ##2: #H2; napply (or2_intro2 … H2)
+ ##| ##1: #H2; nrewrite > H1 in H:(%);
+ nrewrite > H2;
+ #H; nelim (H (refl_eq …))
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqstrid : ∀sid1,sid2.sid1 ≠ sid2 → eq_strId sid1 sid2 = false.
+ #sid1; nelim sid1; #s1; #n1;
+ #sid2; nelim sid2; #s2; #n2;
+ #H; nchange with (((eq_str s1 s2) ⊗ (eq_nat n1 n2)) = false);
+ napply (or2_elim (s1 ≠ s2) (n1 ≠ n2) ? (strid_destruct … H) …);
+ ##[ ##1: #H1; nrewrite > (neq_to_neqstr … H1); nnormalize; napply refl_eq
+ ##| ##2: #H1; nrewrite > (neq_to_neqnat … H1);
+ nrewrite > (symmetric_andbool (eq_str s1 s2) false);
+ nnormalize; napply refl_eq
+ ##]
+nqed.