Apply and3I with
17d4e.. = 17d4e..,
fb516.. ChurchBoolFal,
fb516.. ChurchBoolTru leaving 3 subgoals.
Let x0 of type (CT2 (ι → ι → ι)) → (CT2 (ι → ι → ι)) → ο be given.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_5066d1b2b30c335c067f01ac13f147e53d00378a90e5b6ab1432446a8181f6dd.
The subproof is completed by applying unknownprop_4b2c4a0487c2b1a228c5d07bbf352ffca25633bec988b0f94ee850e02347e107.