Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_8e9afa6cbe34c70175f6c4dbdd044465af8aeced2be56c04dd43afb3a9abc68a with
x1,
4ae4a.. x0,
x2,
∃ x3 . and (x2 = prim3 x3) (aa8d2.. x0 x1 x3) leaving 4 subgoals.
Apply unknownprop_11171438c9340577bc5ca6838eccea0ebdb4279227053bf618ee42741f7851b4 with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply H2 with
∃ x3 . and (x2 = prim3 x3) (aa8d2.. x0 x1 x3).
Apply FalseE with
x2 = x1 ⟶ ∃ x3 . and (x2 = prim3 x3) (aa8d2.. x0 x1 x3).
Apply unknownprop_2602cf2bdb1e417af7ff1134e4c9ee68b103b598c85667d3a4d01fe3c406ee63 with
x0.
The subproof is completed by applying H3.
Apply H2 with
∃ x3 . and (x2 = prim3 x3) (aa8d2.. x0 x1 x3).
Let x3 of type ι be given.
Apply H3 with
∃ x4 . and (x2 = prim3 x4) (aa8d2.. x0 x1 x4).
Let x4 of type ι be given.
Apply H4 with
∃ x5 . and (x2 = prim3 x5) (aa8d2.. x0 x1 x5).
Apply H5 with
aa8d2.. x3 x1 x4 ⟶ ∃ x5 . and (x2 = prim3 x5) (aa8d2.. x0 x1 x5).
Assume H7:
x2 = prim3 x4.
Apply unknownprop_684cb1205e38822a7a824f8a0440cb0f546e66d657860b857331eee8a38df013 with
x0,
x3,
λ x5 x6 . aa8d2.. x5 x1 x4 ⟶ ∃ x7 . and (x2 = prim3 x7) (aa8d2.. x0 x1 x7) leaving 2 subgoals.
The subproof is completed by applying H6.
Let x5 of type ο be given.
Apply H9 with
x4.
Apply andI with
x2 = prim3 x4,
aa8d2.. x0 x1 x4 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H8.