- (o1 = o2 → eq_option T o1 o2 f = true).
- #T; #o1; #o2; #f; #H;
- ncases o1;
- ncases o2;
- ##[ ##1: nnormalize; #H1; napply (refl_eq ??)
- ##| ##2: #H1; #H2; nelim (option_destruct_none_some ?? H2)
- ##| ##3: #H1; #H2; nelim (option_destruct_some_none ?? H2)
- ##| ##4: #x1; #x2; #H1;
- nrewrite > (option_destruct ??? H1);
- nnormalize;
- nrewrite > (H x1 x1 (refl_eq ??));
+ (op1 = op2 → eq_option T op1 op2 f = true).
+ #T; #op1; #op2; #f; #H;
+ napply (option_ind T ??? op1);
+ napply (option_ind T ??? op2);
+ nnormalize;
+ ##[ ##1: #H1; napply (refl_eq ??)
+ ##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1)
+ ##| ##3: #a; #H1; nelim (option_destruct_some_none ?? H1)
+ ##| ##4: #a; #a0; #H1;
+ nrewrite > (option_destruct_some_some ??? H1);
+ nrewrite > (H a a (refl_eq ??));