Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_d4b086cd91c37b32bf1c8961308be7f50bc527a9bea045cb93ec3985b2d19bb6 with
λ x3 x4 : ι → ι → ι . In (Inj1 x2) (x4 x0 x1).
Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with
Repl x0 (λ x3 . Inj0 x3),
Repl x1 (λ x3 . Inj1 x3),
Inj1 x2.
Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with
x1,
Inj1,
x2.
The subproof is completed by applying H0.