Let x0 of type ι be given.
Let x1 of type ο be given.
Assume H0:
∀ x2 : ι → ι . inj 0 x0 x2 ⟶ x1.
Apply H0 with
λ x2 . 0.
Apply andI with
∀ x2 . x2 ∈ 0 ⟶ 0 ∈ x0,
∀ x2 . x2 ∈ 0 ⟶ ∀ x3 . x3 ∈ 0 ⟶ 0 = 0 ⟶ x2 = x3 leaving 2 subgoals.
Let x2 of type ι be given.
Assume H1: x2 ∈ 0.
Apply FalseE with
0 ∈ x0.
Apply EmptyE with
x2.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H1: x2 ∈ 0.
Apply FalseE with
∀ x3 . x3 ∈ 0 ⟶ 0 = 0 ⟶ x2 = x3.
Apply EmptyE with
x2.
The subproof is completed by applying H1.