constructor
case a.x.e_p.h
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
⊢ Setoid.r i k ↔ Setoid.r j k
case a.x.e_p.h.mp
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
⊢ Setoid.r i k → Setoid.r j k

case a.x.e_p.h.mpr
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
⊢ Setoid.r j k → Setoid.r i k