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