λ(_ : Type) →
λ(_ : Optional _) →
  merge { None = True, Some = λ(_ : _@1) → False } _