Let x0 of type ι be given.
Apply unknownprop_d0b18a67181e900ea67f7a0ba30a861268ef122d83dee9e0402983f02611aa3f with
x0,
d634d.. x0 ∈ real leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply H3 with
λ x3 x4 . d634d.. x4 ∈ real.
Apply unknownprop_fb49976af43b10d0ce8aeb3d9ab418005490959b10197c6c1e0102ac4ae81973 with
x1,
x2,
λ x3 x4 . x4 ∈ real leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H2.