Theorem: TEq.all_equal (Katydid/Std/Tipe.lean)

State before:
α✝ : Type u_1
x y : α✝
p q : x ≡ y
⊢ p = q
Tactic:
cases p
State after:
case refl
α✝ : Type u_1
x : α✝
q : x ≡ x
⊢ refl x = q

State before:
case refl
α✝ : Type u_1
x : α✝
q : x ≡ x
⊢ refl x = q
Tactic:
cases q
State after:
case refl.refl
α✝ : Type u_1
x : α✝
⊢ refl x = refl x

State before:
case refl.refl
α✝ : Type u_1
x : α✝
⊢ refl x = refl x
Tactic:
rfl
State after:
no goals