Theorem: TEq.all_tequal (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:
apply refl
State after:
no goals