max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add simp theorem heq_eq_eq

Browse source
This commit is contained in:
Leonardo de Moura 2022-02-24 13:44:58 -08:00
parent b134b9a3a4
commit 8131aa5a64
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/SimpLemmas.lean
View file

@ -148,3 +148,5 @@ theorem dite_congr {s : Decidable b} [Decidable c]
@[simp] theorem Nat.beq_to_eq (a b : Nat) : ((a == b) = true) = (a = b) := by simp [BEq.beq]
@[simp] theorem Nat.not_beq_to_not_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) := by simp [BEq.beq]
@[simp] theorem heq_eq_eq {α : Sort u} (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq