Theorem disused_eq

Proof
01. 1 ⊢ ∀x. x = y → A, hypo.
02. 1 ⊢ y = y → A, uq_elim 1.
03. ⊢ y = y, eq_refl.
04. 1 ⊢ A, subj_elim 2 3.
disused_eq. ⊢ (∀x. x = y → A) → A, subj_intro 4.

Dependencies
The given proof depends on one axiom:
eq_refl.