*response*.txt

option_applicative = 
{|
pure := Some;
ap := option_ap;
identity_law := fun (a : Type) (x : option a) =>
                match
                  x as o return (option_ap (Some identity) o = identity o)
                with
                | Some a0 => eq_refl
                | None => eq_refl
                end;
composition_law := fun (a b : Type) (x : option (a -> b)) =>
                   match
                     x as o
                     return
                       (forall (y : option (a -> a)) (z : option a),
                        option_ap (option_ap (option_ap (Some compose) o) y)
                          z = option_ap o (option_ap y z))
                   with
                   | Some b0 =>
                       fun y : option (a -> a) =>
                       match
                         y as o
                         return
                           (forall z : option a,
                            option_ap
                              (option_ap (option_ap (Some compose) (Some b0))
                                 o) z = option_ap (Some b0) (option_ap o z))
                       with
                       | Some a0 =>
                           fun z : option a =>
                           match
                             z as o
                             return
                               (option_ap
                                  (option_ap
                                     (option_ap (Some compose) (Some b0))
                                     (Some a0)) o =
                                option_ap (Some b0) (option_ap (Some a0) o))
                           with
                           | Some a1 => eq_refl
                           | None => eq_refl
                           end
                       | None =>
                           fun z : option a =>
                           match
                             z as o
                             return
                               (option_ap
                                  (option_ap
                                     (option_ap (Some compose) (Some b0))
                                     None) o =
                                option_ap (Some b0) (option_ap None o))
                           with
                           | Some a0 => eq_refl
                           | None => eq_refl
                           end
                       end
                   | None =>
                       fun (y : option (a -> a)) (z : option a) =>
                       match
                         z as o
                         return
                           (option_ap
                              (option_ap (option_ap (Some compose) None) y) o =
                            option_ap None (option_ap y o))
                       with
                       | Some a0 =>
                           match
                             y as o
                             return
                               (option_ap
                                  (option_ap (option_ap (Some compose) None)
                                     o) (Some a0) =
                                option_ap None (option_ap o (Some a0)))
                           with
                           | Some a1 => eq_refl
                           | None => eq_refl
                           end
                       | None =>
                           match
                             y as o
                             return
                               (option_ap
                                  (option_ap (option_ap (Some compose) None)
                                     o) None =
                                option_ap None (option_ap o None))
                           with
                           | Some a0 => eq_refl
                           | None => eq_refl
                           end
                       end
                   end;
homomorphism_law := fun (a b : Type) (fn : a -> b) (x : a) => eq_refl;
interchange_law := fun (a b : Type) (x : a) (u : option (a -> b)) =>
                   match
                     u as o
                     return
                       (option_ap o (Some x) =
                        option_ap (Some (fun f : a -> b => f x)) o)
                   with
                   | Some b0 => eq_refl
                   | None => eq_refl
                   end |}
     : applicative option