| pf |
|---|
Apply andI with struct_b_b_r_e_e real_struct, unpack_b_b_r_e_e_o real_struct (λ x0 . λ x1 x2 : ι → ι → ι . λ x3 : ι → ι → ο . λ x4 x5 . explicit_Reals x0 x4 x5 x1 x2 x3) leaving 2 subgoals.
Apply pack_struct_b_b_r_e_e_I with real, add_SNo, mul_SNo, SNoLe, 0, 1 leaving 4 subgoals.
The subproof is completed by applying real_add_SNo.
The subproof is completed by applying real_mul_SNo.
The subproof is completed by applying real_0.
The subproof is completed by applying real_1.
Apply RealsStruct_unpack_eq with real, add_SNo, mul_SNo, SNoLe, 0, 1, λ x0 x1 : ο . x1.
The subproof is completed by applying explicit_Reals_real.
■ |
|