Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 80242.. x0.
Let x1 of type ι be given.
Assume H1: prim1 x1 (56ded.. (e4431.. x0)).
Assume H2: x1 = x0.
Apply unknownprop_2c27682abc32e1c8a2160a07043a81afe1f256df4f0472edf3cf11efdcea8609 with x0, False leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H3: ordinal (e4431.. x0).
Assume H4: 1beb9.. (e4431.. x0) x0.
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with e4431.. x0, x1, False leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H1.
Assume H5: prim1 (e4431.. x1) (e4431.. x0).
Assume H6: ordinal (e4431.. x1).
Assume H7: 80242.. x1.
Assume H8: 1beb9.. (e4431.. x1) x1.
Apply In_irref with e4431.. x1.
Apply H2 with λ x2 x3 . prim1 (e4431.. x1) (e4431.. x3).
The subproof is completed by applying H5.
■