Theorem: Primrec.decide_eq_iff (Logic/Vorspiel/Computability.lean)

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
p : Prop
inst✝ : Decidable p
b : Bool
⊢ decide p = b ↔ (p ↔ b = true)
Tactic:
cases b <;> simp
State after:
no goals