Apply unknownprop_ebb79863848e46632cd8c07c8999ac06e4b72b6f254794a2b50220d88403d9cf with
struct_r leaving 3 subgoals.
Let x0 of type ι be given.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_82d75d63f26b09ba7055fe0e3dd6cbd0c974eae3e394476d956067df4f96debf.
The subproof is completed by applying unknownprop_32580ce54fffb5b46927efd90ca1dd97b55002b701a978a208d8cf738022c071.