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

State before:
α : Type u_1
x : Option α
xs : List (Option α)
⊢ first (x :: xs) = HOrElse.hOrElse x fun x => first xs
Tactic:
cases x <;> rfl
State after:
no goals