Apply unknownprop_885912b9bf5d57996dd171d0ae8acb2a108c6e54f48c2b0ffc8b58f100f1bbea with
struct_u leaving 2 subgoals.
Let x0 of type ι be given.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_3e48cfeebcb9f353ad22fcbdda6c6e2151b73e5e40a75364d1fcc60d4e5e1461.