funext k
case e_i.e_val.x.e_p
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
j' : Fin n
hj' : (Fin.find? fun b => decide (Setoid.r j b)) = some j'
⊢ (fun b => decide (Setoid.r i b)) = fun b => decide (Setoid.r j b)
case e_i.e_val.x.e_p.h
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
j' : Fin n
hj' : (Fin.find? fun b => decide (Setoid.r j b)) = some j'
k : Fin n
⊢ decide (Setoid.r i k) = decide (Setoid.r j k)