unfold AGMProofSystemInstantiation.soundness AGMProofSystemInstantiation.verify AGMProofSystemInstantiation.proof_element_G1_as_poly AGMProofSystemInstantiation.proof_element_G2_as_poly
F : Type
inst✝ : Field F
⊢ AGMProofSystemInstantiation.soundness F ToySnark (WitEntries → F)
    (fun stmt wit =>
      wit WitEntries.A * stmt StmtEntries.y = stmt StmtEntries.z ∨
        wit WitEntries.B * stmt StmtEntries.x = stmt StmtEntries.z)
    fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β)
F : Type
inst✝ : Field F
⊢ ∀ (stmt : ToySnark.Stmt) (prover : AGMProofSystemInstantiation.Prover F ToySnark),
    ((∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0) ∧
        ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
          (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
                ToySnark.ListSRSElements_G1).sum =
            (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
                ToySnark.ListSRSElements_G2).sum) →
      (fun stmt wit =>
          wit WitEntries.A * stmt StmtEntries.y = stmt StmtEntries.z ∨
            wit WitEntries.B * stmt StmtEntries.x = stmt StmtEntries.z)
        stmt
        ((fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover)