simp_rw [ToySnark] at eqn
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
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
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqn :
  { Stmt := StmtEntries → F, Sample := Option Vars, SRSElements_G1 := SRS_Elements_G1_Idx,
          ListSRSElements_G1 := [SRS_Elements_G1_Idx.α, SRS_Elements_G1_Idx.β], SRSElements_G2 := SRS_Elements_G2_Idx,
          ListSRSElements_G2 := [SRS_Elements_G2_Idx.α, SRS_Elements_G2_Idx.β],
          SRSElementValue_G1 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_G1_Idx.α => X Vars_α
            | SRS_Elements_G1_Idx.β => X Vars_β,
          SRSElementValue_G2 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_G2_Idx.α => X Vars_α
            | SRS_Elements_G2_Idx.β => X Vars_β,
          Proof_G1 := Proof_G1_Idx, ListProof_G1 := [Proof_G1_Idx.Pf], Proof_G2 := Proof_G2_Idx, ListProof_G2 := [],
          EqualityChecks := Unit, Pairings := fun x => PairingsIdx,
          ListPairings := fun x => [PairingsIdx.lhs, PairingsIdx.rhs],
          verificationPairingSRS_G1 := fun stmt x i SRS_idx =>
            match i with
            | PairingsIdx.lhs => 0
            | PairingsIdx.rhs =>
              match SRS_idx with
              | SRS_Elements_G1_Idx.α => stmt StmtEntries.z
              | SRS_Elements_G1_Idx.β => 0,
          verificationPairingSRS_G2 := fun stmt x i SRS_idx =>
            match i with
            | PairingsIdx.lhs =>
              match SRS_idx with
              | SRS_Elements_G2_Idx.α => stmt StmtEntries.x
              | SRS_Elements_G2_Idx.β => stmt StmtEntries.y
            | PairingsIdx.rhs =>
              match SRS_idx with
              | SRS_Elements_G2_Idx.α => 0
              | SRS_Elements_G2_Idx.β => -1,
          verificationPairingProof_G1 := fun stmt x i pf =>
            match i with
            | PairingsIdx.lhs => 1
            | PairingsIdx.rhs => 0,
          verificationPairingProof_G2 := fun stmt x i pf => 0, Identified_Proof_Elems := [] }.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