Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ο be given.
Assume H0: ∀ x1 : ι → ι → ι . (∃ x2 x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p EquivReln BinRelnHom struct_id struct_comp x1 x2 x3 x4)x0.
Apply H0 with 3fa3a...
Let x1 of type ο be given.
Assume H1: ∀ x2 : ι → ι → ι . (∃ x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p EquivReln BinRelnHom struct_id struct_comp 3fa3a.. x2 x3 x4)x1.
Apply H1 with λ x2 x3 . lam (ap x2 0) (λ x4 . Inj0 x4).
Let x2 of type ο be given.
Assume H2: ∀ x3 : ι → ι → ι . (∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p EquivReln BinRelnHom struct_id struct_comp 3fa3a.. (λ x5 x6 . lam (ap x5 0) (λ x7 . Inj0 x7)) x3 x4)x2.
Apply H2 with λ x3 x4 . lam (ap x4 0) (λ x5 . Inj1 x5).
Let x3 of type ο be given.
Assume H3: ∀ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p EquivReln BinRelnHom struct_id struct_comp 3fa3a.. (λ x5 x6 . lam (ap x5 0) (λ x7 . Inj0 x7)) (λ x5 x6 . lam (ap x6 0) (λ x7 . Inj1 x7)) x4x3.
Apply H3 with λ x4 x5 x6 x7 x8 . lam (setsum (ap x4 0) (ap x5 0)) (λ x9 . combine_funcs (ap x4 0) (ap x5 0) (λ x10 . ap x7 x10) (λ x10 . ap x8 x10) x9).
Apply unknownprop_8014f2189a8e9a90722a83ab5f5b4d52ecd6d5c686aac8aa2eb5343a4f9f7780 with EquivReln leaving 2 subgoals.
Let x4 of type ι be given.
Assume H4: EquivReln x4.
Apply H4 with struct_r x4.
Assume H5: struct_r x4.
Assume H6: unpack_r_o x4 (λ x5 . λ x6 : ι → ι → ο . and (and (∀ x7 . x7x5x6 x7 x7) (∀ x7 . x7x5∀ x8 . x8x5x6 x7 x8x6 x8 x7)) (∀ x7 . x7x5∀ x8 . x8x5∀ x9 . x9x5x6 x7 x8x6 x8 x9x6 x7 x9)).
The subproof is completed by applying H5.
Let x4 of type ι be given.
Let x5 of type ι be given.
Assume H4: EquivReln x4.
Assume H5: EquivReln x5.
Apply unknownprop_6402afcf89af96ded942e84b9859aeeef4ba7eaef1979737905398451311e541 with x4, λ x6 . EquivReln (3fa3a.. x6 x5) leaving 2 subgoals.
The subproof is completed by applying H4.
Let x6 of type ι be given.
Let x7 of type ιιο be given.
Assume H6: ∀ x8 . x8x6x7 x8 x8.
Assume H7: ∀ x8 . x8x6∀ x9 . x9x6x7 x8 x9x7 x9 x8.
Assume H8: ∀ x8 . x8x6∀ x9 . x9x6∀ x10 . x10x6x7 x8 x9x7 x9 x10x7 x8 x10.
Apply unknownprop_6402afcf89af96ded942e84b9859aeeef4ba7eaef1979737905398451311e541 with x5, λ x8 . EquivReln (3fa3a.. (pack_r x6 x7) x8) leaving 2 subgoals.
The subproof is completed by applying H5.
Let x8 of type ι be given.
Let x9 of type ιιο be given.
Assume H9: ∀ x10 . x10x8x9 x10 x10.
Assume H10: ∀ x10 . ...∀ x11 . ...x9 x10 x11x9 x11 x10.
...