Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_bebd867283cf8e42ab0a6fcae40b7b03bd53172bba6a0231eb1c5875aaddede9 with
x0,
x1,
prim0 (aa8d2.. (4ae4a.. x0) x1),
prim0 (aa8d2.. (4ae4a.. x0) x1) = prim3 (prim0 (aa8d2.. x0 x1)) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_90bcc02ecc46b92df3edbe0008c0f8bb530ab6a017204b007fade1bade9af775 with
4ae4a.. x0,
x1.
Apply unknownprop_11171438c9340577bc5ca6838eccea0ebdb4279227053bf618ee42741f7851b4 with
x0.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply H1 with
prim0 (aa8d2.. (4ae4a.. x0) x1) = prim3 (prim0 (aa8d2.. x0 x1)).
Apply H2 with
λ x3 x4 . x4 = prim3 (prim0 (aa8d2.. x0 x1)).
Apply unknownprop_9c1354c1627b000b8714ed09b0e535b241e3434601d3939b6f5f152d11f41e1c with
x1,
x0,
prim0 (aa8d2.. x0 x1),
x2 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_90bcc02ecc46b92df3edbe0008c0f8bb530ab6a017204b007fade1bade9af775 with
x0,
x1.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply L4 with
λ x3 x4 . prim3 x2 = prim3 x4.
Let x3 of type ι → ι → ο be given.
The subproof is completed by applying H5.