no goals
α : Type u_1
β : Type ?u.131924
γ : Type ?u.131927
δ : Type ?u.131930
σ : Type ?u.131933
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : Bool → Bool → α
x✝ : Bool × Bool
a b : Bool
⊢ (bif (a, b).fst then f true (a, b).snd else f false (a, b).snd) = f (a, b).fst (a, b).snd
cases a <;> rfl