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_d69e51cf98d725801d3c48c79c52281c3ff7cc9a4590111d9bd4316b558f0db1 with OrderedFieldStruct.
The subproof is completed by applying L0.
■