Theorem: HFSet.normalize_eq (Hfzfa.lean)

State before:
atoms : Type u_1
inst✝ : DecidableEq atoms
⊢ normalize = fun s => { val := s, property := (_ : s = s) }
Tactic:
ext s : 2
State after:
case h.a
atoms : Type u_1
inst✝ : DecidableEq atoms
s : HFSet atoms
⊢ ↑(normalize s) = ↑{ val := s, property := (_ : s = s) }

State before:
case h.a
atoms : Type u_1
inst✝ : DecidableEq atoms
s : HFSet atoms
⊢ ↑(normalize s) = ↑{ val := s, property := (_ : s = s) }
Tactic:
exact (normalize s).prop
State after:
no goals