theorem ofBool_1_iff_true {b : Bool} : BitVec.ofBool b = 1#1 ↔ b = true

theorem ofBool_0_iff_false {b : Bool} : BitVec.ofBool b = 0#1 ↔ ¬b = true

theorem List.dropLast_nodup {X : Type u_1} (l : List X) : l.Nodup → l.dropLast.Nodup

@[simp]

theorem Array.not_elem_back_pop {X : Type u_1} (a : Array X) (x : X) : a.toList.Nodup → a.back? = some x → ¬x ∈ a.pop

theorem Array.back?_mem {X : Type u_1} (a : Array X) (x : X) : a.back? = some x → x ∈ a

theorem Array.not_elem_back_pop_list {X : Type u_1} (a : Array X) (x : X) : a.toList.Nodup → a.back? = some x → ¬x ∈ a.toList.dropLast

theorem Array.back_mem {X : Type u_1} (a : Array X) (x : X) : a.back? = some x → x ∈ a

theorem Array.mem_of_mem_pop {α : Type u_1} (a : Array α) (x : α) : x ∈ a.pop → x ∈ a

theorem Array.mem_push {α : Type u_1} (a : Array α) (x : α) (y : α) : x ∈ a.push y → x ∈ a ∨ x = y

theorem Std.HashMap.keys_nodup {K : Type u_1} {V : Type u_2} [BEq K] [Hashable K] (m : Std.HashMap K V) : m.keys.Nodup

@[simp]

theorem Std.HashMap.mem_keys_iff_mem {K : Type u_1} {V : Type u_2} [BEq K] [Hashable K] (m : Std.HashMap K V) (k : K) : k ∈ m.keys ↔ k ∈ m

theorem Std.HashMap.mem_keys_insert_new {K : Type u_1} {V : Type u_2} {v : V} [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] (m : Std.HashMap K V) (k : K) : k ∈ m.insert k v

theorem Std.HashMap.mem_keys_insert_old {K : Type u_1} {V : Type u_2} {v : V} [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] (m : Std.HashMap K V) (k : K) (k' : K) : k ∈ m → k ∈ m.insert k' v

theorem Std.HashMap.get?_none_not_mem {K : Type u_1} {V : Type u_2} [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] (m : Std.HashMap K V) (k : K) : m.get? k = none → ¬k ∈ m

theorem Std.HashMap.insert_keys_perm_new {K : Type u_1} {V : Type u_2} [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] (m : Std.HashMap K V) (k : K) (v : V) : ¬k ∈ m → (m.insert k v).keys.Perm (k :: m.keys)