Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Let x3 of type ι → ι be given.
Let x4 of type ι be given.
Apply unknownprop_1a2baecd136edc7de9ce039d67aaa286a9dcf8e2bec22b679c6c9114229bd217 with
λ x5 x6 : ι → ι → (ι → ι) → (ι → ι) → ι → ι . x6 x0 x1 x2 x3 (Inj0 x4) = x2 x4.
Apply unknownprop_05a8fb1492e1d649432d99059efe6cb5519f68cbf274db02d816fcaae9af18ba with
x4,
λ x5 x6 . If_i (Inj0 x4 = Inj0 x6) (x2 x6) (x3 x6) = x2 x4.
Apply unknownprop_6f44febdf8a865ee94133af873e3c2941a931de6ac80968301360290e02ca608 with
Inj0 x4 = Inj0 x4,
x2 x4,
x3 x4.
Let x5 of type ι → ι → ο be given.
The subproof is completed by applying H0.