Theorem: MvQPF.List.typeext (Qpf/Builtins/List.lean)

State before:
α : Sort u_1
f g : α → Sort u_2
f_eq_g : f = g
⊢ ((a : α) → f a) = ((a : α) → g a)
Tactic:
cases f_eq_g
State after:
case refl
α : Sort u_1
f : α → Sort u_2
⊢ ((a : α) → f a) = ((a : α) → f a)

State before:
case refl
α : Sort u_1
f : α → Sort u_2
⊢ ((a : α) → f a) = ((a : α) → f a)
Tactic:
rfl
State after:
no goals