rintro ⟨h₁, h₂⟩
case a.mp
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
⊢ JudgePair.Agree r p c ∧ p.Distinct →
    ∃ a,
      ((JudgePair.Agree r (AgreedTriple.judgePair a) (AgreedTriple.contestant a) ∧
            (AgreedTriple.judgePair a).Distinct) ∧
          AgreedTriple.contestant a = c) ∧
        a.2 = p
case a.mp.intro
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
h₁ : JudgePair.Agree r p c
h₂ : p.Distinct
⊢ ∃ a,
    ((JudgePair.Agree r (AgreedTriple.judgePair a) (AgreedTriple.contestant a) ∧ (AgreedTriple.judgePair a).Distinct) ∧
        AgreedTriple.contestant a = c) ∧
      a.2 = p