Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H1: prim1 x2 x0.
Assume H2: 1beb9.. x2 x1.
Apply H2 with prim1 x1 (56ded.. x0).
Assume H3: Subq x1 (472ec.. x2).
Assume H4: ∀ x3 . prim1 x3 x2 ⟶ exactly1of2 (prim1 ((λ x4 . 15418.. x4 (91630.. (4ae4a.. 4a7ef..))) x3) x1) (prim1 x3 x1).
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with e5b72.. (472ec.. x0), λ x3 . ∃ x4 . and (prim1 x4 x0) (1beb9.. x4 x3), x1 leaving 2 subgoals.
Apply unknownprop_85c22e88a806aabda7246f27ac458442bcb94ac25cc9a3616a68cf646d95941d with 472ec.. x0, x1.
Apply Subq_tra with x1, 472ec.. x2, 472ec.. x0 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_5813163ff7fa03d61d24c49d410e2bda481a277587cdabb44464165443a4046d with x2, x0.
Apply H0 with Subq x2 x0.
Assume H5: TransSet x0.
Assume H6: ∀ x3 . prim1 x3 x0 ⟶ TransSet x3.
Apply H5 with x2.
The subproof is completed by applying H1.
Let x3 of type ο be given.
Assume H5: ∀ x4 . and (prim1 x4 x0) (1beb9.. x4 x1) ⟶ x3.
Apply H5 with x2.
Apply andI with prim1 x2 x0, 1beb9.. x2 x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
■