no goals
α : Type u_1
β : Type ?u.115916
γ : Type ?u.115919
δ : Type ?u.115922
σ : Type ?u.115925
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
o : Option α
⊢ (Option.casesOn (id o) false fun b => true) = Option.isSome o
cases o <;> rfl