nlemma bsymmetric_eqoption :
∀T:Type.∀o1,o2:option T.∀f:T → T → bool.
- (boolSymmetric T f) →
+ (symmetricT T bool f) →
(eq_option T o1 o2 f = eq_option T o2 o1 f).
#T; #o1; #o2; #f; #H;
ncases o1;
ncases o1;
ncases o2;
##[ ##1: nnormalize; #H1; napply (refl_eq ??)
- ##| ##2,3: #H1; #H2; nnormalize in H2:(%); nelim (bool_destruct_false_true H2)
+ ##| ##2,3: #H1; #H2; nnormalize in H2:(%); napply (bool_destruct ??? H2)
##| ##4: #x1; #x2; #H1;
nnormalize in H1:(%);
nrewrite > (H ?? H1);