Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ο be given.
Assume H0: x0 (Inj0 0).
Assume H1: x0 (Inj0 (Power 0)).
Assume H2: ∀ x1 x2 . combinator x1 ⟶ x0 x1 ⟶ combinator x2 ⟶ x0 x2 ⟶ x0 ((λ x3 x4 . Inj1 (setsum x3 x4)) x1 x2).
Let x1 of type ι be given.
Apply unknownprop_24d3fab8c5f2be313e198261133fcc4de3913b4e3dd8f154e7592564c2e0ab41 with λ x2 x3 : ι → ο . x3 x1 ⟶ x0 x1.
Assume H3: (λ x2 . ∀ x3 : ι → ο . x3 (Inj0 0) ⟶ x3 (Inj0 (Power 0)) ⟶ (∀ x4 x5 . x3 x4 ⟶ x3 x5 ⟶ x3 (Inj1 (setsum x4 x5))) ⟶ x3 x2) x1.
Claim L4: and (combinator x1) (x0 x1)
Apply H3 with λ x2 . and (combinator x2) (x0 x2) leaving 3 subgoals.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with combinator (Inj0 0), x0 (Inj0 0) leaving 2 subgoals.
The subproof is completed by applying unknownprop_1be6ee89e47bf30db415892dfc0492321aa3b37926a377afe8fdc4c0df645b89.
The subproof is completed by applying H0.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with combinator (Inj0 (Power 0)), x0 (Inj0 (Power 0)) leaving 2 subgoals.
The subproof is completed by applying unknownprop_2def6145ac5421f9112c2d9b9900cdb9fe5a639cc9f5e2053ff582b1b8cee0be.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H4: (λ x4 . and (combinator x4) (x0 x4)) x2.
Assume H5: (λ x4 . and (combinator x4) (x0 x4)) x3.
Apply andE with combinator x2, x0 x2, (λ x4 . and (combinator x4) (x0 x4)) (Inj1 (setsum x2 x3)) leaving 2 subgoals.
The subproof is completed by applying H4.
Assume H6: combinator x2.
Assume H7: x0 x2.
Apply andE with combinator x3, x0 x3, (λ x4 . and (combinator x4) (x0 x4)) (Inj1 (setsum x2 x3)) leaving 2 subgoals.
The subproof is completed by applying H5.
Assume H8: combinator x3.
Assume H9: x0 x3.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with combinator ((λ x4 x5 . Inj1 (setsum x4 x5)) x2 x3), x0 ((λ x4 x5 . Inj1 (setsum x4 x5)) x2 x3) leaving 2 subgoals.
Apply unknownprop_640ecaf2a8c271a844d2072fe17fde7f6008bced6f0262b37c69e34afaea64bc with x2, x3 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
Apply H2 with x2, x3 leaving 4 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Apply unknownprop_896ccc9f209efa8a895211d65adb5a90348b419f100f6ab5e9762ce4d7fa9cc1 with combinator x1, x0 x1.
The subproof is completed by applying L4.
■