Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ο be given.
Apply UnionE_impred with
94f9e.. 48ef8.. (λ x3 . prim0 (aa8d2.. x3 x0)),
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with
48ef8..,
λ x4 . prim0 (aa8d2.. x4 x0),
x3,
x2 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Apply H1 with
x4 leaving 2 subgoals.
Apply unknownprop_03f5f7248b8d06fe27b9a4f75f4e437d5e9b43a9092733e8b3f6dcfe61f5e308 with
x4.
The subproof is completed by applying H4.
Apply H5 with
λ x5 x6 . prim1 x1 x5.
The subproof is completed by applying H2.