- (eq_option T o1 o2 f = eq_option T o2 o1 f).
- #T; #o1; #o2; #f; #H;
- napply (option_ind T ??? o1);
- napply (option_ind T ??? o2);
+ (eq_option T op1 op2 f = eq_option T op2 op1 f).
+ #T; #op1; #op2; #f; #H;
+ napply (option_ind T ??? op1);
+ napply (option_ind T ??? op2);