Apply and3I with
5d5d8.. = 5d5d8..,
fb516.. ChurchBoolTru,
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_4b2c4a0487c2b1a228c5d07bbf352ffca25633bec988b0f94ee850e02347e107.
The subproof is completed by applying unknownprop_4b2c4a0487c2b1a228c5d07bbf352ffca25633bec988b0f94ee850e02347e107.