Theorem: WType.SubWType.cast_mk (Logic/Vorspiel/W.lean)

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s s' : ℕ
hs : s + 1 = s' + 1
a : α
f : β a → SubWType β s
i : β a
⊢ s = s'
Tactic:
apply Nat.succ_inj'.mp hs
State after:
no goals