Theorem: PartialComposition.comp_with_all_none (TheoremProvingLean/inductive_types.lean)

State before:
α β γ : Type
f : β → Option γ
x : α
⊢ comp_partial f all_none x = Option.none
Tactic:
simp [comp_partial, all_none]
State after:
no goals