Let x0 of type ο be given.

Apply xm with x0, prim1 (If_i x0 (4ae4a.. 4a7ef..) 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..)) leaving 2 subgoals.

Assume H0: x0.

Apply If_i_1 with x0, 4ae4a.. 4a7ef.., 4a7ef.., λ x1 x2 . prim1 x2 (4ae4a.. (4ae4a.. 4a7ef..)) leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying unknownprop_e256c3837ff221325e66d4c83283618d462d76cb96bca463e1abd4876bf63511.

Assume H0: not x0.

Apply If_i_0 with x0, 4ae4a.. 4a7ef.., 4a7ef.., λ x1 x2 . prim1 x2 (4ae4a.. (4ae4a.. 4a7ef..)) leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying unknownprop_94c438c3f41134cd86e0be06a85b5e5b3aa8448f9221f51d2dfe9b1364042f49.

■

Proofgold Proof