theorem
Array.eq_of_isEqvAux
{α : Type u_1}
[inst : DecidableEq α]
(a : Array α)
(b : Array α)
(hsz : Array.size a = Array.size b)
(i : Nat)
(hi : i ≤ Array.size a)
(heqv : Array.isEqvAux a b hsz (fun x y => decide (x = y)) i = true)
(j : Nat)
(low : i ≤ j)
(high : j < Array.size a)
:
Array.get a { val := j, isLt := high } = Array.get b { val := j, isLt := (_ : j < Array.size b) }
theorem
Array.isEqvAux_self
{α : Type u_1}
[inst : DecidableEq α]
(a : Array α)
(i : Nat)
:
Array.isEqvAux a a (_ : Array.size a = Array.size a) (fun x y => decide (x = y)) i = true
theorem
Array.isEqv_self
{α : Type u_1}
[inst : DecidableEq α]
(a : Array α)
:
(Array.isEqv a a fun x y => decide (x = y)) = true