Apply unknownprop_546459d2e02981984519c87d69c9085ebffaa0d7c4326fca643e2a1b93719e6a with
λ x0 x1 : ι → ι . ∀ x2 x3 . In x3 (x1 x2) ⟶ or (In x3 x2) (x3 = x2).
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with
x0,
Sing x0,
x1,
or (In x1 x0) (x1 = x0) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
In x1 x0,
x1 = x0.
The subproof is completed by applying H1.
Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with
In x1 x0,
x1 = x0.
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
x0,
x1.
The subproof is completed by applying H1.