Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_70ac04d26d82d55a8a7aa1e3e5b0320484a1911a0615cda02457d07c571bd97b with
x0,
λ x2 x3 . In x1 x3 ⟶ or (x1 = 0) (∃ x4 . and (In x4 x0) (x1 = Inj1 x4)).
Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with
Sing 0,
Repl x0 (λ x2 . Inj1 x2),
x1,
or (x1 = 0) (∃ x2 . and (In x2 x0) (x1 = Inj1 x2)) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
x1 = 0,
∃ x2 . and (In x2 x0) (x1 = Inj1 x2).
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
0,
x1.
The subproof is completed by applying H1.
Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with
x1 = 0,
∃ x2 . and (In x2 x0) (x1 = Inj1 x2).
Apply unknownprop_74e6ddb76e51f556d0e4a910f649c4782bc9cb375d38baef38a8c05a47e8ef22 with
x0,
Inj1,
x1.
The subproof is completed by applying H1.