Theorem: Subtype.eq_iff (FormalSystems/Chomsky/Regular/TotalDFA.lean)

State before:
α qs : Type
M : DFA α qs
p : α → Prop
x y : Subtype p
h : x = y
⊢ ↑x = ↑y
Tactic:
rw [h]
State after:
no goals