Theorem: Option.first_pure (GMLInit/Data/Option.lean)

State before:
α : Type u_1
x : Option α
⊢ first [x] = x
Tactic:
cases x <;> rfl
State after:
no goals