diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index c2d345489d..4e8ae36f98 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -176,6 +176,24 @@ theorem optParam_eq (α : Sort u) (default : α) : optParam α default = α := r
 
 infix:50 " != " => bne
 
+class LawfulBEq (α : Type u) [BEq α] : Prop where
+  eq_of_beq : (a b : α) → (a == b) = true → a = b
+
+theorem eq_of_beq [BEq α] [LawfulBEq α] {a b : α} (h : (a == b) = true) : a = b :=
+  LawfulBEq.eq_of_beq a b h
+
+instance : LawfulBEq Bool where
+  eq_of_beq a b h := by cases a <;> cases b <;> first | rfl | contradiction
+
+instance : LawfulBEq Nat where
+  eq_of_beq _ _ h := of_decide_eq_true h
+
+instance : LawfulBEq Char where
+  eq_of_beq _ _  h := of_decide_eq_true h
+
+instance : LawfulBEq String where
+  eq_of_beq _ _  h := of_decide_eq_true h
+
 /- Logical connectives an equality -/
 
 def implies (a b : Prop) := a → b
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 5534ad57a2..a77e0b9926 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -472,4 +472,16 @@ def minimum? [LE α] [DecidableRel (@LE.le α _)] : List α → Option α
   | []    => none
   | a::as => some <| as.foldl min a
 
+instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
+  eq_of_beq as bs := by
+    induction as generalizing bs with
+    | nil => intro h; cases bs <;> first | rfl | contradiction
+    | cons a as ih =>
+      cases bs with
+      | nil => intro h; contradiction
+      | cons b bs =>
+        simp [BEq.beq, List.beq]
+        intro ⟨h₁, h₂⟩
+        exact ⟨eq_of_beq h₁, ih _ h₂⟩
+
 end List
diff --git a/src/Init/Data/Prod.lean b/src/Init/Data/Prod.lean
new file mode 100644
index 0000000000..6b192a4e3d
--- /dev/null
+++ b/src/Init/Data/Prod.lean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import Init.SimpLemmas
+
+instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β) where
+  eq_of_beq a b h := by cases a; cases b; simp [BEq.beq] at h; have ⟨h₁, h₂⟩ := h; rw [eq_of_beq h₁, eq_of_beq h₂]