Id tree Special Sound

theorem id_treeSpecialSound {Statement Witness : Type} [Nonempty Witness]    (S : ChallengeTreeShape (!p[] : ProtocolSpec 0))    (rel : Set (Statement × Witness)) :    (Verifier.id (oSpec := oSpec) (Statement := Statement)).treeSpecialSound      init impl S rel rel := by  -- For each statement, some candidate witness works as soon as any witness exists.  have hpick : ∀ stmt : Statement, ∃ w : Witness, (∃ w', (stmt, w') ∈ rel) → (stmt, w) ∈ rel := by    intro stmt    rcases or_not (p := ∃ w', (stmt, w') ∈ rel) with ⟨w, hw⟩ | h    · exact ⟨w, fun _ => hw⟩    · exact ⟨Nonempty.some inferInstance, fun hex => absurd hex h⟩  refine treeSpecialSound_of_isEmpty_challengeIdx init impl S Verifier.id rel rel    (fun stmt _ => (hpick stmt).choose) ?_  intro stmtIn tr hAcc  have hlang : stmtIn ∈ rel.language :=    mem_of_pure_accepting init impl Verifier.id stmtIn tr rel.language stmtIn rfl hAcc  exact (hpick stmtIn).choose_spec ((Set.mem_language_iff rel stmtIn).1 hlang)