α : Type u_1
β : Type ?u.358941
γ : Type ?u.358944
σ : Type ?u.358947
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n
this : Primcodable { a // id a < n } := Primcodable.subtype (_ : PrimrecPred fun a => id a < n)
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec f
α : Type u_1
β : Type ?u.358941
γ : Type ?u.358944
σ : Type ?u.358947
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec f
letI : Primcodable { a // id a < n } := Primcodable.subtype (nat_lt.comp .id (const _))
no goals
α : Type u_1
β : Type ?u.358941
γ : Type ?u.358944
σ : Type ?u.358947
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n
this : Primcodable { a // id a < n } := Primcodable.subtype (_ : PrimrecPred fun a => id a < n)
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec f
exact (Iff.trans (by rfl) subtype_val_iff).trans (of_equiv_iff _)
no goals
α : Type u_1
β : Type ?u.358941
γ : Type ?u.358944
σ : Type ?u.358947
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n
this : Primcodable { a // id a < n } := Primcodable.subtype (_ : PrimrecPred fun a => id a < n)
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec fun a => ↑(↑Fin.equivSubtype (f a))
rfl