Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ο be given.
Assume H0: ∀ x1 : ι → ι → ι . (∃ x2 x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p PtdPred UnaryPredHom struct_id struct_comp x1 x2 x3 x4) ⟶ x0.
Apply H0 with 20e9b...
Let x1 of type ο be given.
Assume H1: ∀ x2 : ι → ι → ι . (∃ x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p PtdPred UnaryPredHom struct_id struct_comp 20e9b.. 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 PtdPred UnaryPredHom struct_id struct_comp 20e9b.. (λ 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 PtdPred UnaryPredHom struct_id struct_comp 20e9b.. (λ x5 x6 . lam (ap x5 0) (λ x7 . Inj0 x7)) (λ x5 x6 . lam (ap x6 0) (λ x7 . Inj1 x7)) x4 ⟶ x3.
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_eb8fa85f1ab6d587c913965e3b03d2a9bd8d29f88f55fc57c7ee9d90282aeead with PtdPred leaving 2 subgoals.
Let x4 of type ι be given.
Assume H4: PtdPred x4.
Apply H4 with struct_p x4.
Assume H5: struct_p x4.
Assume H6: unpack_p_o x4 (λ x5 . λ x6 : ι → ο . ∃ x7 . and (x7 ∈ x5) (x6 x7)).
The subproof is completed by applying H5.
Let x4 of type ι be given.
Let x5 of type ι be given.
Assume H4: PtdPred x4.
Assume H5: PtdPred x5.
Apply unknownprop_c86200a2eefb0ff844f50b29d5cbeaa2ee14856a2db63542bcbf63218f0d0f1e with x4, λ x6 . PtdPred (20e9b.. x6 x5) leaving 2 subgoals.
The subproof is completed by applying H4.
Let x6 of type ι be given.
Let x7 of type ι → ο be given.
Let x8 of type ι be given.
Assume H6: x8 ∈ x6.
Assume H7: x7 x8.
Apply unknownprop_c86200a2eefb0ff844f50b29d5cbeaa2ee14856a2db63542bcbf63218f0d0f1e with x5, λ x9 . PtdPred (20e9b.. (pack_p x6 x7) x9) leaving 2 subgoals.
The subproof is completed by applying H5.
Let x9 of type ι be given.
Let x10 of type ι → ο be given.
Let x11 of type ι be given.
Assume H8: x11 ∈ x9.
Assume H9: x10 x11.
Apply unknownprop_b136686cda57813ec105d14134466864c52e8c5ca85ea4790197540126814cf6 with x6, x7, x9, x10, λ x12 x13 . PtdPred x13.
Apply unknownprop_2576d2815b46016e5e13a9989b4e9789629d83c56ed1c92a4cda0de077a20752 with setsum x6 x9, λ x12 . or (and (x12 = Inj0 (Unj x12)) (x7 (Unj x12))) (and (x12 = Inj1 (Unj x12)) (x10 (Unj x12))).
Let x12 of type ο be given.
Assume H10: ∀ x13 . and (x13 ∈ setsum x6 x9) (or (and (x13 = Inj0 (Unj x13)) (x7 (Unj x13))) (and (x13 = Inj1 (Unj x13)) (x10 (Unj x13)))) ⟶ x12.
Apply H10 with Inj0 x8.
Apply andI with Inj0 x8 ∈ setsum x6 x9, or (and (Inj0 x8 = Inj0 (Unj (Inj0 x8))) (x7 (Unj (Inj0 x8)))) (and (Inj0 x8 = Inj1 ...) ...) leaving 2 subgoals.
...
...
■