have eqn := eqns ()
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns : ∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0
null :
  ∀ 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 prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      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.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns : ∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0
null :
  ∀ 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
eqn : ToySnark.check_poly prover stmt () = 0
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      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.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z