| pf |
|---|
Apply unknownprop_712520f713b96d5afd10321cea9a3c978868fc53aa35a29461e902d5b5a4ba79 with λ x0 . True, HomSet, λ x0 . lam_id x0, λ x0 x1 x2 x3 x4 . lam_comp x0 x3 x4, Permutation, UnaryFuncHom, struct_id, struct_comp, λ x0 . pack_u (setprod int x0) (λ x1 . lam 2 (λ x2 . If_i (x2 = 0) (add_SNo (ap x1 0) 1) (ap x1 1))), λ x0 x1 x2 . lam (setprod int x0) (λ x3 . lam 2 (λ x4 . If_i (x4 = 0) (ap x3 0) (ap x2 (ap x3 1)))), λ x0 . ap x0 0, λ x0 x1 x2 . x2, λ x0 . lam x0 (λ x1 . lam 2 (λ x2 . If_i (x2 = 0) 0 x1)), λ x0 . unpack_u_i x0 (λ x1 . λ x2 : ι → ι . lam (setprod int x1) (λ x3 . If_i (SNoLt (ap x3 0) 0) (1319b.. (minus_SNo (ap x3 0)) (inv x1 x2) (ap x3 1)) (1319b.. (ap x3 0) x2 (ap x3 1)))) leaving 5 subgoals.
Apply unknownprop_3d05796578cdc17ebd2096167db48ecef934256d250d1637eb5dd67225cdfe05 with λ x0 . True, HomSet, λ x0 . lam_id x0, λ x0 x1 x2 x3 x4 . lam_comp x0 x3 x4, Permutation, UnaryFuncHom, struct_id, struct_comp, λ x0 . pack_u (setprod int x0) (λ x1 . lam 2 (λ x2 . If_i (x2 = 0) (add_SNo (ap x1 0) 1) (ap x1 1))), λ x0 x1 x2 . lam (setprod int 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_97a117a3ef894b9fb1eb62c8aa64ff80223ce0478dc6c7c7a52d9ae80a2a2a33.
■ |
|