no goals
α : Type u_1
β : Type ?u.131673
γ : Type ?u.131676
δ : Type ?u.131679
σ : Type ?u.131682
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : Bool → α
b : Bool
⊢ (bif id b then f true else f false) = f b
cases b <;> rfl