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