Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_70ac04d26d82d55a8a7aa1e3e5b0320484a1911a0615cda02457d07c571bd97b with
x0,
λ x2 x3 . In (Inj1 x1) x3.
Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with
Sing 0,
Repl x0 (λ x2 . Inj1 x2),
Inj1 x1.
Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with
x0,
Inj1,
x1.
The subproof is completed by applying H0.