simp [comp_partial, all_none]
α β γ : Type
g : α → Option β
x : α
⊢ comp_partial all_none g x = Option.none
α β γ : Type
g : α → Option β
x : α
⊢ (match g x with
    | Option.none => Option.none
    | Option.some y => Option.none) =
    Option.none