∀ (motive : Option Bool → Option Bool → Sort u_1) (x : Option Bool) (h_1 : (x : Option Bool) → motive (some false) x)
  (h_2 : (x : Option Bool) → motive x (some false)) (h_3 : (x : Option Bool) → motive (some true) x)
  (h_4 : (x : Option Bool) → motive x (some true)) (h_5 : (x x_1 : Option Bool) → motive x x_1),
  (x = some false → False) →
    (match x, some false with
      | some false, x => h_1 x
      | x, some false => h_2 x
      | some true, x => h_3 x
      | x, some true => h_4 x
      | x, x_2 => h_5 x x_2) =
      h_2 x