Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ο be given.
Assume H0: ∀ x1 . x0 x1 ⟶ struct_b x1.
Assume H1: ∀ x1 x2 x3 x4 . x0 x1 ⟶ x0 x2 ⟶ MagmaHom x1 x2 x3 ⟶ MagmaHom x1 x2 x4 ⟶ x0 (32592.. x1 x2 x3 x4).
Let x1 of type ο be given.
Assume H2: ∀ x2 : ι → ι → ι → ι → ι . (∃ x3 : ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 MagmaHom struct_id struct_comp x2 x3 x4) ⟶ x1.
Apply H2 with 32592...
Let x2 of type ο be given.
Assume H3: ∀ x3 : ι → ι → ι → ι → ι . (∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 MagmaHom struct_id struct_comp 32592.. x3 x4) ⟶ x2.
Apply H3 with λ x3 x4 x5 x6 . lam {x7 ∈ ap x3 0|ap x5 x7 = ap x6 x7} (λ x7 . x7).
Let x3 of type ο be given.
Assume H4: ∀ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 MagmaHom struct_id struct_comp 32592.. (λ x5 x6 x7 x8 . lam {x9 ∈ ap x5 0|ap x7 x9 = ap x8 x9} (λ x9 . x9)) x4 ⟶ x3.
Apply H4 with λ x4 x5 x6 x7 x8 x9 . lam (ap x8 0) (λ x10 . ap x9 x10).
Let x4 of type ι be given.
Let x5 of type ι be given.
Assume H5: x0 x4.
Assume H6: x0 x5.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H7: MagmaHom x4 x5 x6.
Assume H8: MagmaHom x4 x5 x7.
Apply H0 with x4, λ x8 . ... ⟶ ... ⟶ ∀ x9 : ο . (... ⟶ ... ⟶ (∀ x10 . ... ⟶ ∀ x11 . ... ⟶ struct_comp x10 x8 x5 x6 x11 = struct_comp x10 x8 x5 ... ... ⟶ and (and (MagmaHom x10 (32592.. x8 x5 x6 x7) ((λ x12 x13 x14 x15 x16 x17 . lam (ap x16 0) (λ x18 . ap x17 x18)) x8 x5 x6 x7 x10 x11)) (struct_comp x10 (32592.. x8 x5 x6 x7) x8 ((λ x12 x13 x14 x15 . lam {x16 ∈ ap x12 0|ap x14 x16 = ap x15 x16} (λ x16 . x16)) x8 x5 x6 x7) ((λ x12 x13 x14 x15 x16 x17 . lam (ap x16 0) (λ x18 . ap x17 x18)) x8 x5 x6 x7 x10 x11) = x11)) (∀ x12 . MagmaHom x10 (32592.. x8 x5 x6 x7) x12 ⟶ struct_comp x10 (32592.. x8 x5 x6 x7) x8 ((λ x13 x14 x15 x16 . lam {x17 ∈ ap x13 0|ap x15 x17 = ap x16 x17} (λ x17 . x17)) x8 x5 x6 x7) x12 = x11 ⟶ x12 = (λ x13 x14 x15 x16 x17 x18 . lam (ap x17 0) (λ x19 . ap x18 x19)) x8 x5 x6 x7 x10 x11)) ⟶ x9) ⟶ x9, ... leaving 5 subgoals.
...
...
...
...
...
■