Theorem inj_elim

Proof
01. 1 ⊢ inj f X Y, hypo.
02. 2 ⊢ a ∈ X, hypo.
03. 3 ⊢ b ∈ X, hypo.
04. 1 ⊢ ∀a. ∀b. a ∈ X → b ∈ X → app f a = app f b → a = b,
  lsubj_conj_elimr inj_equi 1.
05. 1 ⊢ ∀b. a ∈ X → b ∈ X → app f a = app f b → a = b, uq_elim 4.
06. 1 ⊢ a ∈ X → b ∈ X → app f a = app f b → a = b, uq_elim 5.
07. 1, 2 ⊢ b ∈ X → app f a = app f b → a = b, subj_elim 6 2.
08. 1, 2, 3 ⊢ app f a = app f b → a = b, subj_elim 7 3.
inj_elim. ⊢ inj f X Y →
  a ∈ X → b ∈ X → app f a = app f b → a = b, subj_intro_iii 8.