Apply and3I with
271f3.. = 271f3..,
64789.. a4575..,
64789.. a4575.. leaving 3 subgoals.
Let x0 of type (CT2 (CT2 (ι → ι → ι))) → (CT2 (CT2 (ι → ι → ι))) → ο be given.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_ca69d5590f16a82b3262090a8a8e845f4d382952a1b28456e8910491ba455305.
The subproof is completed by applying unknownprop_ca69d5590f16a82b3262090a8a8e845f4d382952a1b28456e8910491ba455305.