Apply unknownprop_eb47bb5cd73cad8b4ef0b3375f134d111d4de0e7e5fceab966d004fbffa38e8d with
struct_b leaving 2 subgoals.
Let x0 of type ι be given.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_baf3fc1e43a364c6a747235fea11365553a8a91f3fbc9bcc7c3dbf5bc88e8597.