simp [orElse_assoc, ih]
case cons
α : Type u_1
ys : List (Option α)
x : Option α
xs : List (Option α)
ih : first (xs ++ ys) = HOrElse.hOrElse (first xs) fun x => first ys
⊢ first (x :: xs ++ ys) = HOrElse.hOrElse (first (x :: xs)) fun x => first ys
no goals