REPred iff decoded pred

lemma _root_.REPred.iff_decoded_pred {α : Type*} [Primcodable α] {A : α → Prop} :    REPred A ↔ REPred fun n : ℕ ↦ (Encodable.decode (α := α) n).elim False A := by  constructor  · intro hA    have hbind : Partrec fun n : ℕ =>        (Encodable.decode (α := α) n : Part α).bind          fun a => Part.assert (A a) fun _ => Part.some () :=      (Computable.ofOption Computable.decode).bind (hA.comp Computable.snd).to₂    refine (Partrec.dom_re hbind).of_eq fun n => ?_    rcases h : Encodable.decode (α := α) n with _ | a <;> simp [Part.assert]  · intro hg    refine REPred.of_eq (p := fun a => (Encodable.decode (α := α) (Encodable.encode a)).elim False A)      (hg.comp Computable.encode) fun a => ?_    simp [Encodable.encodek]