napply refl_eq
##]
nqed.
+
+nlemma decidable_option : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:option T.decidable (x = y).
+ #T; #H; #x; nelim x;
+ ##[ ##1: #y; ncases y;
+ ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+ ##| ##2: #yy; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H1; napply (option_destruct_none_some T … H1)
+ ##]
+ ##| ##2: #xx; #y; ncases y;
+ ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H2; napply (option_destruct_some_none T … H2)
+ ##| ##2: #yy; nnormalize; napply (or2_elim (xx = yy) (xx ≠ yy) ? (H …));
+ ##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H2; napply (H1 (option_destruct_some_some T … H2))
+ ##| ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+ nrewrite > H1; napply refl_eq
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqoption :
+∀T.∀op1,op2:option T.∀f:T → T → bool.
+ (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
+ (op1 ≠ op2 → eq_option T op1 op2 f = false).
+ #T; #op1; nelim op1;
+ ##[ ##1: #op2; ncases op2;
+ ##[ ##1: nnormalize; #f; #H; #H1; nelim (H1 (refl_eq …))
+ ##| ##2: #yy; #f; #H; nnormalize; #H1; napply refl_eq
+ ##]
+ ##| ##2: #xx; #op2; ncases op2;
+ ##[ ##1: #f; #H; nnormalize; #H1; napply refl_eq
+ ##| ##2: #yy; #f; #H; nnormalize; #H1; napply (H xx yy …);
+ nnormalize; #H2; nrewrite > H2 in H1:(%); #H1;
+ napply (H1 (refl_eq …))
+ ##]
+ ##]
+nqed.
+
+nlemma neqoption_to_neq :
+∀T.∀op1,op2:option T.∀f:T → T → bool.
+ (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
+ (eq_option T op1 op2 f = false → op1 ≠ op2).
+ #T; #op1; nelim op1;
+ ##[ ##1: #op2; ncases op2;
+ ##[ ##1: nnormalize; #f; #H; #H1; napply (bool_destruct … H1)
+ ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (option_destruct_none_some T … H2)
+ ##]
+ ##| ##2: #xx; #op2; ncases op2;
+ ##[ ##1: nnormalize; #f; #H; #H1; #H2; napply (option_destruct_some_none T … H2)
+ ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
+ napply (option_destruct_some_some T … H2)
+ ##]
+ ##]
+nqed.