Verifier coordinate Wise Special Sound

theorem verifier_coordinateWiseSpecialSound [Nonempty WitIn]    (D : CWSSStructure (!p[] : ProtocolSpec 0))    (hRel : ∀ stmtIn witOut,      (mapStmt stmtIn, witOut) ∈ relOut → (stmtIn, mapWitInv stmtIn witOut) ∈ relIn) :    (verifier oSpec mapStmt).coordinateWiseSpecialSound init impl D relIn relOut := by  -- For each input statement, some candidate input witness works as soon as any output witness  -- makes the mapped statement accepted.  have hpick : ∀ stmtIn : StmtIn, ∃ witIn : WitIn,      (∃ witOut, (mapStmt stmtIn, witOut) ∈ relOut) → (stmtIn, witIn) ∈ relIn := by    intro stmtIn    rcases or_not (p := ∃ witOut, (mapStmt stmtIn, witOut) ∈ relOut) with ⟨witOut, hw⟩ | h    · exact ⟨mapWitInv stmtIn witOut, fun _ => hRel stmtIn witOut hw⟩    · exact ⟨Nonempty.some inferInstance, fun hex => absurd hex h⟩  refine Verifier.coordinateWiseSpecialSound_of_isEmpty_challengeIdx init impl D    (verifier oSpec mapStmt) relIn relOut (fun stmtIn _ => (hpick stmtIn).choose) ?_  intro stmtIn tr hAcc  have hlang : mapStmt stmtIn ∈ relOut.language :=    Verifier.mem_of_pure_accepting init impl (verifier oSpec mapStmt) stmtIn tr      relOut.language (mapStmt stmtIn) rfl hAcc  exact (hpick stmtIn).choose_spec ((Set.mem_language_iff _ _).1 hlang)