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 (Inj0 x2) (x4 x0 x1).
Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with
Repl x0 (λ x3 . Inj0 x3),
Repl x1 (λ x3 . Inj1 x3),
Inj0 x2.
Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with
x0,
Inj0,
x2.
The subproof is completed by applying H0.