Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Assume H0: Subq x0 x1.
Assume H1: ∀ x3 . prim1 x3 x1 ⟶ nIn x3 x0 ⟶ prim1 4a7ef.. (x2 x3).
Let x3 of type ι be given.
Assume H2: prim1 x3 (3097a.. x0 (λ x4 . x2 x4)).
Apply unknownprop_e91802ac95034c32a27830a437206af24864b973eefcd7f0fba6473c100b9bd7 with x0, x2, x3, prim1 x3 (3097a.. x1 (λ x4 . x2 x4)) leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H3: ∀ x4 . prim1 x4 x3 ⟶ and (cad8f.. x4) (prim1 (f482f.. x4 4a7ef..) x0).
Assume H4: ∀ x4 . prim1 x4 x0 ⟶ prim1 (f482f.. x3 x4) (x2 x4).
Apply unknownprop_e08a04d424da13101fe4a24b5b4e61037f5c9a4ddbf473297ae7bfacedd63b2c with x1, x2, x3 leaving 2 subgoals.
Let x4 of type ι be given.
Assume H5: prim1 x4 x3.
Apply H3 with x4, and (cad8f.. x4) (prim1 (f482f.. x4 4a7ef..) x1) leaving 2 subgoals.
The subproof is completed by applying H5.
Assume H6: cad8f.. x4.
Assume H7: prim1 (f482f.. x4 4a7ef..) x0.
Apply andI with cad8f.. x4, prim1 (f482f.. x4 4a7ef..) x1 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply H0 with f482f.. x4 4a7ef...
The subproof is completed by applying H7.
Let x4 of type ι be given.
Assume H5: prim1 x4 x1.
Apply xm with prim1 x4 x0, prim1 (f482f.. x3 x4) (x2 x4) leaving 2 subgoals.
Assume H6: prim1 x4 x0.
Apply H4 with x4.
The subproof is completed by applying H6.
Assume H6: nIn x4 x0.
Claim L7: f482f.. x3 x4 = 4a7ef..
Apply unknownprop_737136f881572e1e56d45956970b8a48cb6d97aa65fdd10a73326f0a724af5d2 with x0, x2, x3, λ x5 x6 . f482f.. x5 x4 = 4a7ef.. leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_39bbb446aef706467a6347b64fa9f06781a98b01507cfc573d478167c5f0dd65 with x0, f482f.. x3, x4.
The subproof is completed by applying H6.
Apply L7 with λ x5 x6 . prim1 x6 (x2 x4).
Apply H1 with x4 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
■