Let x0 of type ι be given.
Apply unknownprop_d74508268cf2245bb4de852843c85bf4733bd48f6383eaac9c68dfae0d149115 with
707e2.. (λ x1 . prim1 x1 x0),
x0.
Let x1 of type ι be given.
Apply iffI with
prim1 x1 (707e2.. (λ x2 . prim1 x2 x0)),
prim1 x1 x0 leaving 2 subgoals.
Apply unknownprop_381047c913ae030e9e9942d1a8901abc4d96b713731a5b7b04cd06cd75bdfe7a with
λ x2 . prim1 x2 x0,
x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_e470535d6c827033c9dfdf9bd32865d66aa3967ca3d37f3ae8e6aa53cde5ec29 with x0.
The subproof is completed by applying H0.
Apply unknownprop_ef71c7659631e6712550b179497e8718243f15729bbc2ba1fccf8bb659c5df87 with
λ x2 . prim1 x2 x0,
x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_e470535d6c827033c9dfdf9bd32865d66aa3967ca3d37f3ae8e6aa53cde5ec29 with x0.
The subproof is completed by applying H0.