| pf |
|---|
Apply unknownprop_712520f713b96d5afd10321cea9a3c978868fc53aa35a29461e902d5b5a4ba79 with λ x0 . True, HomSet, λ x0 . lam_id x0, λ x0 x1 x2 x3 x4 . lam_comp x0 x3 x4, struct_u, UnaryFuncHom, struct_id, struct_comp, 340cb.., 9132f.., λ x0 . ap x0 0, λ x0 x1 x2 . x2, 139e8.., 82409.. leaving 5 subgoals.
Apply unknownprop_3d05796578cdc17ebd2096167db48ecef934256d250d1637eb5dd67225cdfe05 with λ x0 . True, HomSet, λ x0 . lam_id x0, λ x0 x1 x2 x3 x4 . lam_comp x0 x3 x4, struct_u, UnaryFuncHom, struct_id, struct_comp, λ x0 . pack_u (setprod omega x0) (λ x1 . lam 2 (λ x2 . If_i (x2 = 0) (ordsucc (ap x1 0)) (ap x1 1))), λ x0 x1 x2 . lam (setprod omega x0) (λ x3 . lam 2 (λ x4 . If_i (x4 = 0) (ap x3 0) (ap x2 (ap x3 1)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_dcf5739aa5fe0adc626fd983737b233fe68652dff14c53b3d75823dcf2542d41.
The subproof is completed by applying unknownprop_5de12671ce5578185e763d350f97672aefc724365fc2efb408ee27de0205dcd6.
Apply unknownprop_795e291855a044d4d636c961caa1600704603cc02e33a7b37aa66e8d7f6512db with λ x0 . True, HomSet, λ x0 . lam_id x0, λ x0 x1 x2 x3 x4 . lam_comp x0 x3 x4, struct_u, UnaryFuncHom, struct_id, struct_comp, λ x0 . pack_u (setprod omega x0) (λ x1 . lam 2 (λ x2 . If_i (x2 = 0) (ordsucc (ap x1 0)) (ap x1 1))), λ x0 x1 x2 . lam (setprod omega x0) (λ x3 . lam 2 (λ x4 . If_i (x4 = 0) (ap x3 0) (ap x2 (ap x3 1)))) leaving 4 subgoals.
Let x0 of type ι be given.
Assume H6: (λ x1 . True) x0. Apply pack_struct_u_I with setprod omega x0, λ x1 . lam 2 (λ x2 . If_i (x2 = 0) (ordsucc (ap x1 0)) (ap x1 1)).
The subproof is completed by applying L0 with x0.
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H6: (λ x3 . True) x0. Assume H7: (λ x3 . True) x1. ■ |
|