Let x0 of type ι be given.
Apply Field_of_RealsStruct_3 with
x0,
λ x1 x2 . explicit_Field (field0 x0) x2 (ap (Field_of_RealsStruct x0) 4) (decode_b (ap (Field_of_RealsStruct x0) 1)) (decode_b (ap (Field_of_RealsStruct x0) 2)).
Apply Field_of_RealsStruct_4 with
x0,
λ x1 x2 . explicit_Field (field0 x0) (field4 x0) x2 (decode_b (ap (Field_of_RealsStruct x0) 1)) (decode_b (ap (Field_of_RealsStruct x0) 2)).
Apply unknownprop_020ff441acf63956db89023138d2e3bf192b2578e8bfb819c9422a66b469b129 with
field0 x0,
field4 x0,
RealsStruct_one x0,
field1b x0,
field2b x0,
decode_b (ap (Field_of_RealsStruct x0) 1),
decode_b (ap (Field_of_RealsStruct x0) 2) leaving 3 subgoals.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply pack_b_b_e_e_1_eq2 with
field0 x0,
field1b x0,
field2b x0,
field4 x0,
RealsStruct_one x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply pack_b_b_e_e_2_eq2 with
field0 x0,
field1b x0,
field2b x0,
field4 x0,
RealsStruct_one x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply explicit_Field_of_RealsStruct with
x0.
The subproof is completed by applying H0.