Theorem: collapseSRSElement_G1_soundness (FormalSnarksProject/Transformations/Transformations.lean)

State before:
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
⊢ AGMProofSystemInstantiation.soundness F (collapseSRSElement_G1 𝓟 twin1 twin2) Wit relation extractor
Tactic:
intros stmt agm checks_pass
State after:
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
checks_pass : (collapseSRSElement_G1 𝓟 twin1 twin2).verify agm stmt
⊢ relation stmt (extractor agm)

State before:
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
checks_pass : (collapseSRSElement_G1 𝓟 twin1 twin2).verify agm stmt
⊢ relation stmt (extractor agm)
Tactic:
rcases checks_pass with ⟨poly_checks_pass, null⟩
State after:
case intro
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (collapseSRSElement_G1 𝓟 twin1 twin2).check_poly agm stmt check_idx = 0
null :
  ∀ pfs ∈ (collapseSRSElement_G1 𝓟 twin1 twin2).Identified_Proof_Elems,
    (collapseSRSElement_G1 𝓟 twin1 twin2).proof_element_G1_as_poly agm pfs.1 =
      (collapseSRSElement_G1 𝓟 twin1 twin2).proof_element_G2_as_poly agm pfs.2
⊢ relation stmt (extractor agm)

State before:
case intro
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (collapseSRSElement_G1 𝓟 twin1 twin2).check_poly agm stmt check_idx = 0
null :
  ∀ pfs ∈ (collapseSRSElement_G1 𝓟 twin1 twin2).Identified_Proof_Elems,
    (collapseSRSElement_G1 𝓟 twin1 twin2).proof_element_G1_as_poly agm pfs.1 =
      (collapseSRSElement_G1 𝓟 twin1 twin2).proof_element_G2_as_poly agm pfs.2
⊢ relation stmt (extractor agm)
Tactic:
apply h_sound
State after:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (collapseSRSElement_G1 𝓟 twin1 twin2).check_poly agm stmt check_idx = 0
null :
  ∀ pfs ∈ (collapseSRSElement_G1 𝓟 twin1 twin2).Identified_Proof_Elems,
    (collapseSRSElement_G1 𝓟 twin1 twin2).proof_element_G1_as_poly agm pfs.1 =
      (collapseSRSElement_G1 𝓟 twin1 twin2).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt

State before:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (collapseSRSElement_G1 𝓟 twin1 twin2).check_poly agm stmt check_idx = 0
null :
  ∀ pfs ∈ (collapseSRSElement_G1 𝓟 twin1 twin2).Identified_Proof_Elems,
    (collapseSRSElement_G1 𝓟 twin1 twin2).proof_element_G1_as_poly agm pfs.1 =
      (collapseSRSElement_G1 𝓟 twin1 twin2).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt
Tactic:
clear h_sound null
State after:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (collapseSRSElement_G1 𝓟 twin1 twin2).check_poly agm stmt check_idx = 0
⊢ 𝓟.verify agm stmt

State before:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (collapseSRSElement_G1 𝓟 twin1 twin2).check_poly agm stmt check_idx = 0
⊢ 𝓟.verify agm stmt
Tactic:
unfold AGMProofSystemInstantiation.verify AGMProofSystemInstantiation.check_poly AGMProofSystemInstantiation.pairing_poly AGMProofSystemInstantiation.proof_element_G1_as_poly AGMProofSystemInstantiation.proof_element_G2_as_poly at *
State after:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G1 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G1 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G2 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G2 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum))
          ((collapseSRSElement_G1 𝓟 twin1 twin2).ListPairings check_idx)).sum =
      0
⊢ (∀ (check_idx : 𝓟.EqualityChecks),
      (List.map
            (fun pairing =>
              ((List.map
                      (fun pf_elem =>
                        MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                          (List.map
                              (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                              𝓟.ListSRSElements_G1).sum)
                      𝓟.ListProof_G1).sum +
                  (List.map
                      (fun SRS_elem =>
                        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G1 SRS_elem)
                      𝓟.ListSRSElements_G1).sum) *
                ((List.map
                      (fun pf_elem =>
                        MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                          (List.map
                              (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                              𝓟.ListSRSElements_G2).sum)
                      𝓟.ListProof_G2).sum +
                  (List.map
                      (fun SRS_elem =>
                        MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G2 SRS_elem)
                      𝓟.ListSRSElements_G2).sum))
            (𝓟.ListPairings check_idx)).sum =
        0) ∧
    ∀ pfs ∈ 𝓟.Identified_Proof_Elems,
      (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pfs.1 SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum =
        (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pfs.2 SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
            𝓟.ListSRSElements_G2).sum

State before:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G1 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G1 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G2 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G2 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum))
          ((collapseSRSElement_G1 𝓟 twin1 twin2).ListPairings check_idx)).sum =
      0
⊢ (∀ (check_idx : 𝓟.EqualityChecks),
      (List.map
            (fun pairing =>
              ((List.map
                      (fun pf_elem =>
                        MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                          (List.map
                              (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                              𝓟.ListSRSElements_G1).sum)
                      𝓟.ListProof_G1).sum +
                  (List.map
                      (fun SRS_elem =>
                        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G1 SRS_elem)
                      𝓟.ListSRSElements_G1).sum) *
                ((List.map
                      (fun pf_elem =>
                        MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                          (List.map
                              (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                              𝓟.ListSRSElements_G2).sum)
                      𝓟.ListProof_G2).sum +
                  (List.map
                      (fun SRS_elem =>
                        MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G2 SRS_elem)
                      𝓟.ListSRSElements_G2).sum))
            (𝓟.ListPairings check_idx)).sum =
        0) ∧
    ∀ pfs ∈ 𝓟.Identified_Proof_Elems,
      (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pfs.1 SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum =
        (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pfs.2 SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
            𝓟.ListSRSElements_G2).sum
Tactic:
constructor
State after:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G1 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G1 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G2 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G2 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum))
          ((collapseSRSElement_G1 𝓟 twin1 twin2).ListPairings check_idx)).sum =
      0
⊢ ∀ (check_idx : 𝓟.EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                            𝓟.ListSRSElements_G1).sum)
                    𝓟.ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        𝓟.SRSElementValue_G1 SRS_elem)
                    𝓟.ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                            𝓟.ListSRSElements_G2).sum)
                    𝓟.ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum))
          (𝓟.ListPairings check_idx)).sum =
      0

case intro.a.right
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G1 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G1 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G2 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G2 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum))
          ((collapseSRSElement_G1 𝓟 twin1 twin2).ListPairings check_idx)).sum =
      0
⊢ ∀ pfs ∈ 𝓟.Identified_Proof_Elems,
    (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pfs.1 SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pfs.2 SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
          𝓟.ListSRSElements_G2).sum

State before:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G1 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G1 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G2 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G2 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum))
          ((collapseSRSElement_G1 𝓟 twin1 twin2).ListPairings check_idx)).sum =
      0
⊢ ∀ (check_idx : 𝓟.EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                            𝓟.ListSRSElements_G1).sum)
                    𝓟.ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        𝓟.SRSElementValue_G1 SRS_elem)
                    𝓟.ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                            𝓟.ListSRSElements_G2).sum)
                    𝓟.ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum))
          (𝓟.ListPairings check_idx)).sum =
      0
Tactic:
intro check_idx
State after:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G1 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G1 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G2 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G2 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum))
          ((collapseSRSElement_G1 𝓟 twin1 twin2).ListPairings check_idx)).sum =
      0
check_idx : 𝓟.EqualityChecks
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0

State before:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
poly_checks_pass :
  ∀ (check_idx : (collapseSRSElement_G1 𝓟 twin1 twin2).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G1 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G1 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G2 stmt check_idx pairing
                            pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                            (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G2 stmt check_idx pairing
                            SRS_elem) *
                        (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                    (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum))
          ((collapseSRSElement_G1 𝓟 twin1 twin2).ListPairings check_idx)).sum =
      0
check_idx : 𝓟.EqualityChecks
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
Tactic:
replace poly_checks_pass := poly_checks_pass check_idx
State after:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G1 stmt check_idx pairing
                          pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                              (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                          (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum)
                  (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G1 stmt check_idx pairing
                          SRS_elem) *
                      (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                  (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G2 stmt check_idx pairing
                          pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                              (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                          (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum)
                  (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G2 stmt check_idx pairing
                          SRS_elem) *
                      (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                  (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum))
        ((collapseSRSElement_G1 𝓟 twin1 twin2).ListPairings check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0

State before:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G1 stmt check_idx pairing
                          pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                              (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                          (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum)
                  (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G1 stmt check_idx pairing
                          SRS_elem) *
                      (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G1 SRS_elem)
                  (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingProof_G2 stmt check_idx pairing
                          pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                              (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                          (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum)
                  (collapseSRSElement_G1 𝓟 twin1 twin2).ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ((collapseSRSElement_G1 𝓟 twin1 twin2).verificationPairingSRS_G2 stmt check_idx pairing
                          SRS_elem) *
                      (collapseSRSElement_G1 𝓟 twin1 twin2).SRSElementValue_G2 SRS_elem)
                  (collapseSRSElement_G1 𝓟 twin1 twin2).ListSRSElements_G2).sum))
        ((collapseSRSElement_G1 𝓟 twin1 twin2).ListPairings check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
Tactic:
unfold collapseSRSElement_G1 at poly_checks_pass
State after:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun srs =>
                                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingProof_G1
                          stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                              { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                                    ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                                    ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                                    SRSElementValue_G1 := fun srs =>
                                      if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                      else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                                    SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                                    ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2,
                                    ListProof_G2 := 𝓟.ListProof_G2, EqualityChecks := 𝓟.EqualityChecks,
                                    Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                                    verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                                    verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                                    verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                                    verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                                    Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G1
                                SRS_elem)
                          { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun srs =>
                                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G1).sum)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun srs =>
                        if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                        else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun srs =>
                                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingSRS_G1
                          stmt check_idx pairing SRS_elem) *
                      { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                            ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                            ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                            SRSElementValue_G1 := fun srs =>
                              if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                              else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                            SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                            ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                            EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                            verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                            verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                            verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                            verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                            Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G1
                        SRS_elem)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun srs =>
                        if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                        else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun srs =>
                                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingProof_G2
                          stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                              { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                                    ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                                    ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                                    SRSElementValue_G1 := fun srs =>
                                      if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                      else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                                    SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                                    ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2,
                                    ListProof_G2 := 𝓟.ListProof_G2, EqualityChecks := 𝓟.EqualityChecks,
                                    Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                                    verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                                    verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                                    verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                                    verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                                    Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G2
                                SRS_elem)
                          { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun srs =>
                                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G2).sum)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun srs =>
                        if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                        else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun srs =>
                                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingSRS_G2
                          stmt check_idx pairing SRS_elem) *
                      { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                            ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                            ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                            SRSElementValue_G1 := fun srs =>
                              if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                              else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                            SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                            ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                            EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                            verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                            verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                            verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                            verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                            Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G2
                        SRS_elem)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun srs =>
                        if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                        else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G2).sum))
        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
              SRSElementValue_G1 := fun srs =>
                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1, ListProof_G1 := 𝓟.ListProof_G1,
              Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2, EqualityChecks := 𝓟.EqualityChecks,
              Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
              verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListPairings
          check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0

State before:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun srs =>
                                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingProof_G1
                          stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                              { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                                    ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                                    ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                                    SRSElementValue_G1 := fun srs =>
                                      if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                      else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                                    SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                                    ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2,
                                    ListProof_G2 := 𝓟.ListProof_G2, EqualityChecks := 𝓟.EqualityChecks,
                                    Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                                    verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                                    verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                                    verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                                    verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                                    Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G1
                                SRS_elem)
                          { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun srs =>
                                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G1).sum)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun srs =>
                        if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                        else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun srs =>
                                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingSRS_G1
                          stmt check_idx pairing SRS_elem) *
                      { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                            ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                            ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                            SRSElementValue_G1 := fun srs =>
                              if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                              else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                            SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                            ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                            EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                            verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                            verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                            verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                            verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                            Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G1
                        SRS_elem)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun srs =>
                        if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                        else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun srs =>
                                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingProof_G2
                          stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                              { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                                    ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                                    ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                                    SRSElementValue_G1 := fun srs =>
                                      if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                      else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                                    SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                                    ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2,
                                    ListProof_G2 := 𝓟.ListProof_G2, EqualityChecks := 𝓟.EqualityChecks,
                                    Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                                    verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                                    verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                                    verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                                    verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                                    Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G2
                                SRS_elem)
                          { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun srs =>
                                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G2).sum)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun srs =>
                        if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                        else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun srs =>
                                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingSRS_G2
                          stmt check_idx pairing SRS_elem) *
                      { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                            ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                            ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                            SRSElementValue_G1 := fun srs =>
                              if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                              else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                            SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                            ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                            EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                            verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                            verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                            verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                            verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                            Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G2
                        SRS_elem)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun srs =>
                        if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                        else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G2).sum))
        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
              SRSElementValue_G1 := fun srs =>
                if srs = twin1 then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs,
              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1, ListProof_G1 := 𝓟.ListProof_G1,
              Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2, EqualityChecks := 𝓟.EqualityChecks,
              Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
              verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListPairings
          check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
Tactic:
simp only [mul_ite, mul_zero] at poly_checks_pass
State after:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            if SRS_elem = twin1 then
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                            else
                              if SRS_elem = twin2 then 0
                              else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    if SRS_elem = twin1 then
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                    else
                      if SRS_elem = twin2 then 0
                      else
                        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0

State before:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            if SRS_elem = twin1 then
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                            else
                              if SRS_elem = twin2 then 0
                              else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    if SRS_elem = twin1 then
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                    else
                      if SRS_elem = twin2 then 0
                      else
                        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
Tactic:
rw [←poly_checks_pass]
State after:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            if SRS_elem = twin1 then
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                            else
                              if SRS_elem = twin2 then 0
                              else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    if SRS_elem = twin1 then
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                    else
                      if SRS_elem = twin2 then 0
                      else
                        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            if SRS_elem = twin1 then
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                            else
                              if SRS_elem = twin2 then 0
                              else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    if SRS_elem = twin1 then
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                    else
                      if SRS_elem = twin2 then 0
                      else
                        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum

State before:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            if SRS_elem = twin1 then
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                            else
                              if SRS_elem = twin2 then 0
                              else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    if SRS_elem = twin1 then
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                    else
                      if SRS_elem = twin2 then 0
                      else
                        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            if SRS_elem = twin1 then
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                            else
                              if SRS_elem = twin2 then 0
                              else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    if SRS_elem = twin1 then
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                    else
                      if SRS_elem = twin2 then 0
                      else
                        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum
Tactic:
clear poly_checks_pass
State after:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            if SRS_elem = twin1 then
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                            else
                              if SRS_elem = twin2 then 0
                              else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    if SRS_elem = twin1 then
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                    else
                      if SRS_elem = twin2 then 0
                      else
                        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum

State before:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            if SRS_elem = twin1 then
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                            else
                              if SRS_elem = twin2 then 0
                              else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    if SRS_elem = twin1 then
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                    else
                      if SRS_elem = twin2 then 0
                      else
                        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum
Tactic:
congr
State after:
case intro.a.left.e_a.e_f
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
⊢ (fun pairing =>
      ((List.map
              (fun pf_elem =>
                MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                  (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                      𝓟.ListSRSElements_G1).sum)
              𝓟.ListProof_G1).sum +
          (List.map
              (fun SRS_elem =>
                MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                  𝓟.SRSElementValue_G1 SRS_elem)
              𝓟.ListSRSElements_G1).sum) *
        ((List.map
              (fun pf_elem =>
                MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                  (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                      𝓟.ListSRSElements_G2).sum)
              𝓟.ListProof_G2).sum +
          (List.map
              (fun SRS_elem =>
                MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                  𝓟.SRSElementValue_G2 SRS_elem)
              𝓟.ListSRSElements_G2).sum)) =
    fun pairing =>
    ((List.map
            (fun pf_elem =>
              MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                (List.map
                    (fun SRS_elem =>
                      if SRS_elem = twin1 then
                        MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                          (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                      else
                        if SRS_elem = twin2 then 0
                        else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                    𝓟.ListSRSElements_G1).sum)
            𝓟.ListProof_G1).sum +
        (List.map
            (fun SRS_elem =>
              if SRS_elem = twin1 then
                MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                  (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
              else
                if SRS_elem = twin2 then 0
                else
                  MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                    𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum) *
      ((List.map
            (fun pf_elem =>
              MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum)
            𝓟.ListProof_G2).sum +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G2 SRS_elem)
            𝓟.ListSRSElements_G2).sum)

State before:
case intro.a.left.e_a.e_f
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
⊢ (fun pairing =>
      ((List.map
              (fun pf_elem =>
                MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                  (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                      𝓟.ListSRSElements_G1).sum)
              𝓟.ListProof_G1).sum +
          (List.map
              (fun SRS_elem =>
                MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                  𝓟.SRSElementValue_G1 SRS_elem)
              𝓟.ListSRSElements_G1).sum) *
        ((List.map
              (fun pf_elem =>
                MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                  (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                      𝓟.ListSRSElements_G2).sum)
              𝓟.ListProof_G2).sum +
          (List.map
              (fun SRS_elem =>
                MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                  𝓟.SRSElementValue_G2 SRS_elem)
              𝓟.ListSRSElements_G2).sum)) =
    fun pairing =>
    ((List.map
            (fun pf_elem =>
              MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                (List.map
                    (fun SRS_elem =>
                      if SRS_elem = twin1 then
                        MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                          (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                      else
                        if SRS_elem = twin2 then 0
                        else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                    𝓟.ListSRSElements_G1).sum)
            𝓟.ListProof_G1).sum +
        (List.map
            (fun SRS_elem =>
              if SRS_elem = twin1 then
                MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                  (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
              else
                if SRS_elem = twin2 then 0
                else
                  MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                    𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum) *
      ((List.map
            (fun pf_elem =>
              MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum)
            𝓟.ListProof_G2).sum +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G2 SRS_elem)
            𝓟.ListSRSElements_G2).sum)
Tactic:
funext pairing
State after:
case intro.a.left.e_a.e_f.h
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ ((List.map
            (fun pf_elem =>
              MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                    𝓟.ListSRSElements_G1).sum)
            𝓟.ListProof_G1).sum +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum) *
      ((List.map
            (fun pf_elem =>
              MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum)
            𝓟.ListProof_G2).sum +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G2 SRS_elem)
            𝓟.ListSRSElements_G2).sum) =
    ((List.map
            (fun pf_elem =>
              MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                (List.map
                    (fun SRS_elem =>
                      if SRS_elem = twin1 then
                        MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                          (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                      else
                        if SRS_elem = twin2 then 0
                        else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                    𝓟.ListSRSElements_G1).sum)
            𝓟.ListProof_G1).sum +
        (List.map
            (fun SRS_elem =>
              if SRS_elem = twin1 then
                MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                  (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
              else
                if SRS_elem = twin2 then 0
                else
                  MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                    𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum) *
      ((List.map
            (fun pf_elem =>
              MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum)
            𝓟.ListProof_G2).sum +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G2 SRS_elem)
            𝓟.ListSRSElements_G2).sum)

State before:
case intro.a.left.e_a.e_f.h
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ ((List.map
            (fun pf_elem =>
              MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                    𝓟.ListSRSElements_G1).sum)
            𝓟.ListProof_G1).sum +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum) *
      ((List.map
            (fun pf_elem =>
              MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum)
            𝓟.ListProof_G2).sum +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G2 SRS_elem)
            𝓟.ListSRSElements_G2).sum) =
    ((List.map
            (fun pf_elem =>
              MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                (List.map
                    (fun SRS_elem =>
                      if SRS_elem = twin1 then
                        MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                          (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                      else
                        if SRS_elem = twin2 then 0
                        else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                    𝓟.ListSRSElements_G1).sum)
            𝓟.ListProof_G1).sum +
        (List.map
            (fun SRS_elem =>
              if SRS_elem = twin1 then
                MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                  (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
              else
                if SRS_elem = twin2 then 0
                else
                  MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                    𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum) *
      ((List.map
            (fun pf_elem =>
              MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum)
            𝓟.ListProof_G2).sum +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G2 SRS_elem)
            𝓟.ListSRSElements_G2).sum)
Tactic:
congr 1
State after:
case intro.a.left.e_a.e_f.h.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
          (fun pf_elem =>
            MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
              (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum)
          𝓟.ListProof_G1).sum +
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
              𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum =
    (List.map
          (fun pf_elem =>
            MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
              (List.map
                  (fun SRS_elem =>
                    if SRS_elem = twin1 then
                      MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                        (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                    else
                      if SRS_elem = twin2 then 0
                      else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum)
          𝓟.ListProof_G1).sum +
      (List.map
          (fun SRS_elem =>
            if SRS_elem = twin1 then
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
            else
              if SRS_elem = twin2 then 0
              else
                MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                  𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum

State before:
case intro.a.left.e_a.e_f.h.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
          (fun pf_elem =>
            MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
              (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum)
          𝓟.ListProof_G1).sum +
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
              𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum =
    (List.map
          (fun pf_elem =>
            MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
              (List.map
                  (fun SRS_elem =>
                    if SRS_elem = twin1 then
                      MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                        (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                    else
                      if SRS_elem = twin2 then 0
                      else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum)
          𝓟.ListProof_G1).sum +
      (List.map
          (fun SRS_elem =>
            if SRS_elem = twin1 then
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
            else
              if SRS_elem = twin2 then 0
              else
                MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                  𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum
Tactic:
congr 1
State after:
case intro.a.left.e_a.e_f.h.e_a.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
        (fun pf_elem =>
          MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
            (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                𝓟.ListSRSElements_G1).sum)
        𝓟.ListProof_G1).sum =
    (List.map
        (fun pf_elem =>
          MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
            (List.map
                (fun SRS_elem =>
                  if SRS_elem = twin1 then
                    MvPolynomial.C (agm.1 pf_elem SRS_elem) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                  else
                    if SRS_elem = twin2 then 0
                    else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                𝓟.ListSRSElements_G1).sum)
        𝓟.ListProof_G1).sum

case intro.a.left.e_a.e_f.h.e_a.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
        (fun SRS_elem =>
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    (List.map
        (fun SRS_elem =>
          if SRS_elem = twin1 then
            MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
              (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
          else
            if SRS_elem = twin2 then 0
            else
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum

State before:
case intro.a.left.e_a.e_f.h.e_a.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
        (fun pf_elem =>
          MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
            (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                𝓟.ListSRSElements_G1).sum)
        𝓟.ListProof_G1).sum =
    (List.map
        (fun pf_elem =>
          MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
            (List.map
                (fun SRS_elem =>
                  if SRS_elem = twin1 then
                    MvPolynomial.C (agm.1 pf_elem SRS_elem) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
                  else
                    if SRS_elem = twin2 then 0
                    else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                𝓟.ListSRSElements_G1).sum)
        𝓟.ListProof_G1).sum
Tactic:
congr
State after:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (fun pf_elem =>
      MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
        (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum) =
    fun pf_elem =>
    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
      (List.map
          (fun SRS_elem =>
            if SRS_elem = twin1 then
              MvPolynomial.C (agm.1 pf_elem SRS_elem) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
            else
              if SRS_elem = twin2 then 0 else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum

State before:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (fun pf_elem =>
      MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
        (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum) =
    fun pf_elem =>
    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
      (List.map
          (fun SRS_elem =>
            if SRS_elem = twin1 then
              MvPolynomial.C (agm.1 pf_elem SRS_elem) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
            else
              if SRS_elem = twin2 then 0 else MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum
Tactic:
funext proof_elem
State after:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f.h
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
proof_elem : 𝓟.Proof_G1
⊢ MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing proof_elem) *
      (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum =
    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing proof_elem) *
      (List.map
          (fun SRS_elem =>
            if SRS_elem = twin1 then
              MvPolynomial.C (agm.1 proof_elem SRS_elem) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
            else
              if SRS_elem = twin2 then 0
              else MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum

State before:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f.h
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
proof_elem : 𝓟.Proof_G1
⊢ MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing proof_elem) *
      (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum =
    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing proof_elem) *
      (List.map
          (fun SRS_elem =>
            if SRS_elem = twin1 then
              MvPolynomial.C (agm.1 proof_elem SRS_elem) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
            else
              if SRS_elem = twin2 then 0
              else MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum
Tactic:
congr 1
State after:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f.h.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
proof_elem : 𝓟.Proof_G1
⊢ (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    (List.map
        (fun SRS_elem =>
          if SRS_elem = twin1 then
            MvPolynomial.C (agm.1 proof_elem SRS_elem) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
          else
            if SRS_elem = twin2 then 0 else MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum

State before:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f.h.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
proof_elem : 𝓟.Proof_G1
⊢ (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    (List.map
        (fun SRS_elem =>
          if SRS_elem = twin1 then
            MvPolynomial.C (agm.1 proof_elem SRS_elem) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
          else
            if SRS_elem = twin2 then 0 else MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum
Tactic:
replace interchangeable := interchangeable proof_elem agm.1
State after:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f.h.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
proof_elem : 𝓟.Proof_G1
interchangeable : agm.1 proof_elem twin1 = agm.1 proof_elem twin2
⊢ (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    (List.map
        (fun SRS_elem =>
          if SRS_elem = twin1 then
            MvPolynomial.C (agm.1 proof_elem SRS_elem) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
          else
            if SRS_elem = twin2 then 0 else MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum

State before:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f.h.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
proof_elem : 𝓟.Proof_G1
interchangeable : agm.1 proof_elem twin1 = agm.1 proof_elem twin2
⊢ (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    (List.map
        (fun SRS_elem =>
          if SRS_elem = twin1 then
            MvPolynomial.C (agm.1 proof_elem SRS_elem) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
          else
            if SRS_elem = twin2 then 0 else MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum
Tactic:
simp only [List.sum_map_ite_eq, nsmul_eq_mul, zero_sub, smul_neg]
State after:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f.h.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
proof_elem : 𝓟.Proof_G1
interchangeable : agm.1 proof_elem twin1 = agm.1 proof_elem twin2
⊢ (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    ↑(List.count twin1 𝓟.ListSRSElements_G1) *
        (MvPolynomial.C (agm.1 proof_elem twin1) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2) -
          if twin1 = twin2 then 0 else MvPolynomial.C (agm.1 proof_elem twin1) * 𝓟.SRSElementValue_G1 twin1) +
      (-(↑(List.count twin2 𝓟.ListSRSElements_G1) *
            (MvPolynomial.C (agm.1 proof_elem twin2) * 𝓟.SRSElementValue_G1 twin2)) +
        (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)

State before:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f.h.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
proof_elem : 𝓟.Proof_G1
interchangeable : agm.1 proof_elem twin1 = agm.1 proof_elem twin2
⊢ (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    ↑(List.count twin1 𝓟.ListSRSElements_G1) *
        (MvPolynomial.C (agm.1 proof_elem twin1) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2) -
          if twin1 = twin2 then 0 else MvPolynomial.C (agm.1 proof_elem twin1) * 𝓟.SRSElementValue_G1 twin1) +
      (-(↑(List.count twin2 𝓟.ListSRSElements_G1) *
            (MvPolynomial.C (agm.1 proof_elem twin2) * 𝓟.SRSElementValue_G1 twin2)) +
        (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)
Tactic:
simp only [hcount1, Nat.cast_one, interchangeable, not_same, ↓reduceIte, one_mul, hcount2]
State after:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f.h.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
proof_elem : 𝓟.Proof_G1
interchangeable : agm.1 proof_elem twin1 = agm.1 proof_elem twin2
⊢ (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    MvPolynomial.C (agm.1 proof_elem twin2) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2) -
        MvPolynomial.C (agm.1 proof_elem twin2) * 𝓟.SRSElementValue_G1 twin1 +
      (-(MvPolynomial.C (agm.1 proof_elem twin2) * 𝓟.SRSElementValue_G1 twin2) +
        (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)

State before:
case intro.a.left.e_a.e_f.h.e_a.e_a.e_a.e_f.h.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
proof_elem : 𝓟.Proof_G1
interchangeable : agm.1 proof_elem twin1 = agm.1 proof_elem twin2
⊢ (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    MvPolynomial.C (agm.1 proof_elem twin2) * (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2) -
        MvPolynomial.C (agm.1 proof_elem twin2) * 𝓟.SRSElementValue_G1 twin1 +
      (-(MvPolynomial.C (agm.1 proof_elem twin2) * 𝓟.SRSElementValue_G1 twin2) +
        (List.map (fun SRS_elem => MvPolynomial.C (agm.1 proof_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)
Tactic:
ring
State after:
no goals

State before:
case intro.a.left.e_a.e_f.h.e_a.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
        (fun SRS_elem =>
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    (List.map
        (fun SRS_elem =>
          if SRS_elem = twin1 then
            MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
              (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2)
          else
            if SRS_elem = twin2 then 0
            else
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum
Tactic:
simp only [List.sum_map_ite_eq, nsmul_eq_mul, zero_sub, smul_neg]
State after:
case intro.a.left.e_a.e_f.h.e_a.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
        (fun SRS_elem =>
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    ↑(List.count twin1 𝓟.ListSRSElements_G1) *
        (MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) *
            (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2) -
          if twin1 = twin2 then 0
          else MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) * 𝓟.SRSElementValue_G1 twin1) +
      (-(↑(List.count twin2 𝓟.ListSRSElements_G1) *
            (MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin2)) +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)

State before:
case intro.a.left.e_a.e_f.h.e_a.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
        (fun SRS_elem =>
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    ↑(List.count twin1 𝓟.ListSRSElements_G1) *
        (MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) *
            (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2) -
          if twin1 = twin2 then 0
          else MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) * 𝓟.SRSElementValue_G1 twin1) +
      (-(↑(List.count twin2 𝓟.ListSRSElements_G1) *
            (MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin2)) +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)
Tactic:
simp only [hcount1, Nat.cast_one, not_same, ↓reduceIte, one_mul, hcount2]
State after:
case intro.a.left.e_a.e_f.h.e_a.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
        (fun SRS_elem =>
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) *
          (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2) -
        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) * 𝓟.SRSElementValue_G1 twin1 +
      (-(MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin2) +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)

State before:
case intro.a.left.e_a.e_f.h.e_a.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
        (fun SRS_elem =>
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) *
          (𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2) -
        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) * 𝓟.SRSElementValue_G1 twin1 +
      (-(MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin2) +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)
Tactic:
rw [mul_add]
State after:
case intro.a.left.e_a.e_f.h.e_a.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
        (fun SRS_elem =>
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) * 𝓟.SRSElementValue_G1 twin1 +
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) * 𝓟.SRSElementValue_G1 twin2 -
        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) * 𝓟.SRSElementValue_G1 twin1 +
      (-(MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin2) +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)

State before:
case intro.a.left.e_a.e_f.h.e_a.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
        (fun SRS_elem =>
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) * 𝓟.SRSElementValue_G1 twin1 +
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) * 𝓟.SRSElementValue_G1 twin2 -
        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1) * 𝓟.SRSElementValue_G1 twin1 +
      (-(MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin2) +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)
Tactic:
simp_rw [interchangeable']
State after:
case intro.a.left.e_a.e_f.h.e_a.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
        (fun SRS_elem =>
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin1 +
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin2 -
        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin1 +
      (-(MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin2) +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)

State before:
case intro.a.left.e_a.e_f.h.e_a.e_a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
hTypeIII : 𝓟.Identified_Proof_Elems = []
inst✝ : DecidableEq 𝓟.SRSElements_G1
twin1 twin2 : 𝓟.SRSElements_G1
not_same : twin1 ≠ twin2
hcount1 : List.count twin1 𝓟.ListSRSElements_G1 = 1
hcount2 : List.count twin2 𝓟.ListSRSElements_G1 = 1
interchangeable : ∀ (idx : 𝓟.Proof_G1) (agm : 𝓟.Proof_G1 → 𝓟.SRSElements_G1 → F), agm idx twin1 = agm idx twin2
interchangeable' :
  ∀ (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx),
    𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin1 = 𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseSRSElement_G1 𝓟 twin1 twin2).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseSRSElement_G1 𝓟 twin1 twin2)
check_idx : 𝓟.EqualityChecks
pairing : 𝓟.Pairings check_idx
⊢ (List.map
        (fun SRS_elem =>
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
        𝓟.ListSRSElements_G1).sum =
    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin1 +
          MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin2 -
        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin1 +
      (-(MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing twin2) * 𝓟.SRSElementValue_G1 twin2) +
        (List.map
            (fun SRS_elem =>
              MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum)
Tactic:
ring
State after:
no goals