Fold Commit Oracle Verifier rbr Knowledge Soundness

theorem foldCommitOracleVerifier_rbrKnowledgeSoundness    (i : Fin ℓ) (hCR : isCommitmentRound ℓ ϑ i) :    (foldCommitOracleVerifier (mp := mp) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)      i hCR).rbrKnowledgeSoundness      init impl      (relIn := roundRelation (mp := mp) 𝔽q β (ϑ:=ϑ)        (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.castSucc)      (relOut := roundRelation (mp := mp) 𝔽q β (ϑ:=ϑ)        (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ)      (rbrKnowledgeError := fun _ => foldKnowledgeError (mp := mp) 𝔽q β (ϑ:=ϑ)        (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i ⟨1, by rfl⟩      ) := by  unfold foldCommitOracleVerifier pSpecFoldCommit  have herr : (fun _ => foldKnowledgeError (mp := mp) 𝔽q β (ϑ := ϑ)      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i ⟨1, by rfl⟩) =      (Sum.elim (foldKnowledgeError (mp := mp) 𝔽q β (ϑ := ϑ)          (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i)        (commitKnowledgeError 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)) ∘        (ChallengeIdx.sumEquiv (pSpec₁ := pSpecFold (L := L) (d := mp.degCombinator + 1))          (pSpec₂ := pSpecCommit 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i)).symm) := by    funext m    simp only [Function.comp, ChallengeIdx.sumEquiv, Equiv.symm]    dsimp    split    · simp [foldKnowledgeError]    · next hlt =>      exfalso      have hv := m.1.isLt      have hp := m.2      simp only [ProtocolSpec.append, Fin.vappend_eq_append, Fin.append, Fin.addCases,        Direction.not_P_to_V_eq_V_to_P] at hp      split at hp <;> simp_all <;> omega  rw [herr]  exact OracleVerifier.append_rbrKnowledgeSoundness _ _      (foldOracleVerifier_rbrKnowledgeSoundness (mp := mp) 𝔽q β i)      (commitOracleVerifier_rbrKnowledgeSoundness 𝔽q β i hCR)