Theorem neq_symm

Proof
01. 1 ⊢ ¬x = y, hypo.
02. 2 ⊢ y = x, hypo.
03. 2 ⊢ x = y, eq_symm 2.
04. 1, 2 ⊢ ⊥, neg_elim 1 3.
05. 1 ⊢ ¬y = x, neg_intro 4.
neq_symm. ⊢ ¬x = y → ¬y = x, subj_intro 5.

Dependencies
The given proof depends on two axioms:
eq_refl, eq_subst.