Oracle Verifier coordinate Wise Special Sound

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