| Some : A → option A.
ndefinition eq_option ≝
-λT.λop1,op2:option T.λf:T → T → bool.
+λT.λf:T → T → bool.λop1,op2:option T.
match op1 with
[ None ⇒ match op2 with [ None ⇒ true | Some _ ⇒ false ]
| Some x1 ⇒ match op2 with [ None ⇒ false | Some x2 ⇒ f x1 x2 ]