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 (5246e.. x0).
Let x2 of type ο be given.
Assume H2: 80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x0 x1 ⟶ x2.
Apply unknownprop_e4362c04e65a765de9cf61045b78be0adc0f9e51a17754420e1088df0891ff67 with 56ded.. (e4431.. x0), λ x3 . 099f3.. x0 x3, x1, x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3: prim1 x1 (56ded.. (e4431.. x0)).
Assume H4: 099f3.. x0 x1.
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with e4431.. x0, x1, x2 leaving 3 subgoals.
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Assume H5: prim1 (e4431.. x1) (e4431.. x0).
Assume H6: ordinal (e4431.. x1).
Assume H7: 80242.. x1.
Assume H8: 1beb9.. (e4431.. x1) x1.
Apply H2 leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
■