Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ∀ x0 . OrderedFieldStruct x0 ⟶ struct_b_b_r_e_e x0
Let x0 of type ι be given.
Assume H0: OrderedFieldStruct x0.
Apply H0 with struct_b_b_r_e_e x0.
Assume H1: struct_b_b_r_e_e x0.
Assume H2: unpack_b_b_r_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 : ι → ι → ο . λ x5 x6 . explicit_OrderedField x1 x5 x6 x2 x3 x4).
The subproof is completed by applying H1.
Apply unknownprop_de2d15ec1a8706291df52b9be0c3b5a1251c48871e332f302880d36281797b83 with OrderedFieldStruct.
The subproof is completed by applying L0.
■