no goals
α : Type u_1
β : Type ?u.17342
γ : Type ?u.17345
δ : Type ?u.17348
f : α → α → α
h : ∀ (a b : α), f a b = a ∨ f a b = b
a b : α
⊢ liftOrGet f (some a) (some b) = some a ∨ liftOrGet f (some a) (some b) = some b
simpa [liftOrGet] using h a b