Theorem: Eq.all_tequal (Katydid/Std/Tipe.lean)

State before:
α✝ : Sort u_1
x y : α✝
p q : x = y
⊢ p = q
Tactic:
cases p
State after:
case refl
α✝ : Sort u_1
x : α✝
q : x = x
⊢ (_ : x = x) = q

State before:
case refl
α✝ : Sort u_1
x : α✝
q : x = x
⊢ (_ : x = x) = q
Tactic:
cases q
State after:
case refl.refl
α✝ : Sort u_1
x : α✝
⊢ (_ : x = x) = (_ : x = x)

State before:
case refl.refl
α✝ : Sort u_1
x : α✝
⊢ (_ : x = x) = (_ : x = x)
Tactic:
apply refl
State after:
no goals