Theorem: String.decEq_refl (SInfinity/Util.lean)

State before:
s : String
⊢ decEq s s = isTrue (_ : s = s)
Tactic:
cases String.decEq s s <;> try contradiction
State after:
case isTrue
s : String
h✝ : s = s
⊢ isTrue h✝ = isTrue (_ : s = s)

State before:
case isTrue
s : String
h✝ : s = s
⊢ isTrue h✝ = isTrue (_ : s = s)
Tactic:
simp
State after:
no goals

State before:
case isFalse
s : String
h✝ : ¬s = s
⊢ isFalse h✝ = isTrue (_ : s = s)
Tactic:
contradiction
State after:
no goals