isEqv

theorem List.isEqv_eq_decide {α : Type u_1} (a : List α) (b : List α) (r : α → α → Bool) : a.isEqv b r = if h : a.length = b.length then decide (∀ (i : Nat) (h' : i < a.length), r a[i] b[i] = true) else false

beq

theorem List.beq_eq_isEqv {α : Type u_1} [BEq α] (a : List α) (b : List α) : a.beq b = a.isEqv b fun (x1 x2 : α) => x1 == x2

theorem List.beq_eq_decide {α : Type u_1} [BEq α] (a : List α) (b : List α) : (a == b) = if h : a.length = b.length then decide (∀ (i : Nat) (h' : i < a.length), (a[i] == b[i]) = true) else false