isEqv

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

beq

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

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