Apply unknownprop_f1192b47b0f464fe58426261d8a7942a16b2719933db53997b39bfd0689be81c with
48ef8..,
e5b72.. 48ef8..,
False leaving 2 subgoals.
The subproof is completed by applying H0.
Let x0 of type ι → ι be given.
Apply unknownprop_52c071ce021437c353fc21d774ed57e005ac90529a902d9369487792de7c7170 with
x0.