Apply unknownprop_92ad80f77e0e0f57984196a1c5b97eaceff60da34aaa2014f3d9d81cba2d8285 with
struct_p leaving 2 subgoals.
Let x0 of type ι be given.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_a8e710c43d2d421a4e74fd1a35a2aa81549a76aa8b6394f6178a5202ccb14044.