Theorem: GGPR.soundness
Proof state before:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI : GGPR.check_poly prover stmt ChecksIdx.CheckI = 0
eqnII : GGPR.check_poly prover stmt ChecksIdx.CheckII = 0
eqnIII : GGPR.check_poly prover stmt ChecksIdx.CheckIII = 0
eqnIV : GGPR.check_poly prover stmt ChecksIdx.CheckIV = 0
eqnV : GGPR.check_poly prover stmt ChecksIdx.CheckV = 0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0
Tactic:
simp_rw [GGPR] at eqnI eqnII eqnIII eqnIV eqnV
Proof state after:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI :
  { Stmt := Fin n_stmt → F, Sample := Option Vars, SRSElements_G1 := SRS_Elements_Idx,
          ListSRSElements_G1 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElements_G2 := SRS_Elements_Idx,
          ListSRSElements_G2 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElementValue_G1 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          SRSElementValue_G2 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          Proof_G1 := Proof_G1_Idx,
          ListProof_G1 := [Proof_G1_Idx.V_mid, Proof_G1_Idx.V_mid', Proof_G1_Idx.W', Proof_G1_Idx.Y, Proof_G1_Idx.H'],
          Proof_G2 := Proof_G2_Idx, ListProof_G2 := [Proof_G2_Idx.W, Proof_G2_Idx.H], EqualityChecks := ChecksIdx,
          Pairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => PairingsI_Idx
            | ChecksIdx.CheckII => PairingsII_Idx
            | ChecksIdx.CheckIII => PairingsIII_Idx
            | ChecksIdx.CheckIV => PairingsIV_Idx
            | ChecksIdx.CheckV => PairingsV_Idx,
          ListPairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => [PairingsI_Idx.lhs, PairingsI_Idx.rhs]
            | ChecksIdx.CheckII => [PairingsII_Idx.lhs, PairingsII_Idx.rhs]
            | ChecksIdx.CheckIII => [PairingsIII_Idx.lhs, PairingsIII_Idx.rhs]
            | ChecksIdx.CheckIV => [PairingsIV_Idx.lhs, PairingsIV_Idx.rhs]
            | ChecksIdx.CheckV => [PairingsV_Idx.lhs, PairingsV_Idx.rhs1, PairingsV_Idx.rhs2],
          verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_v_0 => 1
                | SRS_Elements_Idx.VK_v_stmt k => stmt k
                | x => 0
              | PairingsI_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_t => 1
                | x => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs => 0
              | PairingsII_Idx.rhs => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βw_γ => 1
                | x => 0,
          verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_w_0 => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => -1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_γ => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βv_γ => -1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G1 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid' => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.W' => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.H' => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.Y => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G2 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G2_Idx.W => 1
                | x => 0
              | PairingsI_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckII, i => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0,
          Identified_Proof_Elems := [] }.check_poly
      prover stmt ChecksIdx.CheckI =
    0
eqnII :
  { Stmt := Fin n_stmt → F, Sample := Option Vars, SRSElements_G1 := SRS_Elements_Idx,
          ListSRSElements_G1 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElements_G2 := SRS_Elements_Idx,
          ListSRSElements_G2 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElementValue_G1 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          SRSElementValue_G2 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          Proof_G1 := Proof_G1_Idx,
          ListProof_G1 := [Proof_G1_Idx.V_mid, Proof_G1_Idx.V_mid', Proof_G1_Idx.W', Proof_G1_Idx.Y, Proof_G1_Idx.H'],
          Proof_G2 := Proof_G2_Idx, ListProof_G2 := [Proof_G2_Idx.W, Proof_G2_Idx.H], EqualityChecks := ChecksIdx,
          Pairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => PairingsI_Idx
            | ChecksIdx.CheckII => PairingsII_Idx
            | ChecksIdx.CheckIII => PairingsIII_Idx
            | ChecksIdx.CheckIV => PairingsIV_Idx
            | ChecksIdx.CheckV => PairingsV_Idx,
          ListPairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => [PairingsI_Idx.lhs, PairingsI_Idx.rhs]
            | ChecksIdx.CheckII => [PairingsII_Idx.lhs, PairingsII_Idx.rhs]
            | ChecksIdx.CheckIII => [PairingsIII_Idx.lhs, PairingsIII_Idx.rhs]
            | ChecksIdx.CheckIV => [PairingsIV_Idx.lhs, PairingsIV_Idx.rhs]
            | ChecksIdx.CheckV => [PairingsV_Idx.lhs, PairingsV_Idx.rhs1, PairingsV_Idx.rhs2],
          verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_v_0 => 1
                | SRS_Elements_Idx.VK_v_stmt k => stmt k
                | x => 0
              | PairingsI_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_t => 1
                | x => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs => 0
              | PairingsII_Idx.rhs => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βw_γ => 1
                | x => 0,
          verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_w_0 => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => -1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_γ => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βv_γ => -1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G1 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid' => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.W' => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.H' => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.Y => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G2 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G2_Idx.W => 1
                | x => 0
              | PairingsI_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckII, i => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0,
          Identified_Proof_Elems := [] }.check_poly
      prover stmt ChecksIdx.CheckII =
    0
eqnIII :
  { Stmt := Fin n_stmt → F, Sample := Option Vars, SRSElements_G1 := SRS_Elements_Idx,
          ListSRSElements_G1 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElements_G2 := SRS_Elements_Idx,
          ListSRSElements_G2 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElementValue_G1 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          SRSElementValue_G2 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          Proof_G1 := Proof_G1_Idx,
          ListProof_G1 := [Proof_G1_Idx.V_mid, Proof_G1_Idx.V_mid', Proof_G1_Idx.W', Proof_G1_Idx.Y, Proof_G1_Idx.H'],
          Proof_G2 := Proof_G2_Idx, ListProof_G2 := [Proof_G2_Idx.W, Proof_G2_Idx.H], EqualityChecks := ChecksIdx,
          Pairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => PairingsI_Idx
            | ChecksIdx.CheckII => PairingsII_Idx
            | ChecksIdx.CheckIII => PairingsIII_Idx
            | ChecksIdx.CheckIV => PairingsIV_Idx
            | ChecksIdx.CheckV => PairingsV_Idx,
          ListPairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => [PairingsI_Idx.lhs, PairingsI_Idx.rhs]
            | ChecksIdx.CheckII => [PairingsII_Idx.lhs, PairingsII_Idx.rhs]
            | ChecksIdx.CheckIII => [PairingsIII_Idx.lhs, PairingsIII_Idx.rhs]
            | ChecksIdx.CheckIV => [PairingsIV_Idx.lhs, PairingsIV_Idx.rhs]
            | ChecksIdx.CheckV => [PairingsV_Idx.lhs, PairingsV_Idx.rhs1, PairingsV_Idx.rhs2],
          verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_v_0 => 1
                | SRS_Elements_Idx.VK_v_stmt k => stmt k
                | x => 0
              | PairingsI_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_t => 1
                | x => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs => 0
              | PairingsII_Idx.rhs => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βw_γ => 1
                | x => 0,
          verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_w_0 => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => -1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_γ => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βv_γ => -1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G1 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid' => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.W' => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.H' => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.Y => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G2 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G2_Idx.W => 1
                | x => 0
              | PairingsI_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckII, i => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0,
          Identified_Proof_Elems := [] }.check_poly
      prover stmt ChecksIdx.CheckIII =
    0
eqnIV :
  { Stmt := Fin n_stmt → F, Sample := Option Vars, SRSElements_G1 := SRS_Elements_Idx,
          ListSRSElements_G1 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElements_G2 := SRS_Elements_Idx,
          ListSRSElements_G2 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElementValue_G1 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          SRSElementValue_G2 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          Proof_G1 := Proof_G1_Idx,
          ListProof_G1 := [Proof_G1_Idx.V_mid, Proof_G1_Idx.V_mid', Proof_G1_Idx.W', Proof_G1_Idx.Y, Proof_G1_Idx.H'],
          Proof_G2 := Proof_G2_Idx, ListProof_G2 := [Proof_G2_Idx.W, Proof_G2_Idx.H], EqualityChecks := ChecksIdx,
          Pairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => PairingsI_Idx
            | ChecksIdx.CheckII => PairingsII_Idx
            | ChecksIdx.CheckIII => PairingsIII_Idx
            | ChecksIdx.CheckIV => PairingsIV_Idx
            | ChecksIdx.CheckV => PairingsV_Idx,
          ListPairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => [PairingsI_Idx.lhs, PairingsI_Idx.rhs]
            | ChecksIdx.CheckII => [PairingsII_Idx.lhs, PairingsII_Idx.rhs]
            | ChecksIdx.CheckIII => [PairingsIII_Idx.lhs, PairingsIII_Idx.rhs]
            | ChecksIdx.CheckIV => [PairingsIV_Idx.lhs, PairingsIV_Idx.rhs]
            | ChecksIdx.CheckV => [PairingsV_Idx.lhs, PairingsV_Idx.rhs1, PairingsV_Idx.rhs2],
          verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_v_0 => 1
                | SRS_Elements_Idx.VK_v_stmt k => stmt k
                | x => 0
              | PairingsI_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_t => 1
                | x => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs => 0
              | PairingsII_Idx.rhs => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βw_γ => 1
                | x => 0,
          verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_w_0 => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => -1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_γ => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βv_γ => -1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G1 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid' => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.W' => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.H' => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.Y => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G2 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G2_Idx.W => 1
                | x => 0
              | PairingsI_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckII, i => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0,
          Identified_Proof_Elems := [] }.check_poly
      prover stmt ChecksIdx.CheckIV =
    0
eqnV :
  { Stmt := Fin n_stmt → F, Sample := Option Vars, SRSElements_G1 := SRS_Elements_Idx,
          ListSRSElements_G1 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElements_G2 := SRS_Elements_Idx,
          ListSRSElements_G2 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElementValue_G1 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          SRSElementValue_G2 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          Proof_G1 := Proof_G1_Idx,
          ListProof_G1 := [Proof_G1_Idx.V_mid, Proof_G1_Idx.V_mid', Proof_G1_Idx.W', Proof_G1_Idx.Y, Proof_G1_Idx.H'],
          Proof_G2 := Proof_G2_Idx, ListProof_G2 := [Proof_G2_Idx.W, Proof_G2_Idx.H], EqualityChecks := ChecksIdx,
          Pairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => PairingsI_Idx
            | ChecksIdx.CheckII => PairingsII_Idx
            | ChecksIdx.CheckIII => PairingsIII_Idx
            | ChecksIdx.CheckIV => PairingsIV_Idx
            | ChecksIdx.CheckV => PairingsV_Idx,
          ListPairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => [PairingsI_Idx.lhs, PairingsI_Idx.rhs]
            | ChecksIdx.CheckII => [PairingsII_Idx.lhs, PairingsII_Idx.rhs]
            | ChecksIdx.CheckIII => [PairingsIII_Idx.lhs, PairingsIII_Idx.rhs]
            | ChecksIdx.CheckIV => [PairingsIV_Idx.lhs, PairingsIV_Idx.rhs]
            | ChecksIdx.CheckV => [PairingsV_Idx.lhs, PairingsV_Idx.rhs1, PairingsV_Idx.rhs2],
          verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_v_0 => 1
                | SRS_Elements_Idx.VK_v_stmt k => stmt k
                | x => 0
              | PairingsI_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_t => 1
                | x => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs => 0
              | PairingsII_Idx.rhs => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βw_γ => 1
                | x => 0,
          verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_w_0 => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => -1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_γ => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βv_γ => -1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G1 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid' => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.W' => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.H' => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.Y => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G2 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G2_Idx.W => 1
                | x => 0
              | PairingsI_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckII, i => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0,
          Identified_Proof_Elems := [] }.check_poly
      prover stmt ChecksIdx.CheckV =
    0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0