Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_99ced72b0a1cc72e56a6449ae7f85ace98b316636257ef59b14e002a0cde881d with
x0,
x1,
0,
λ x2 x3 . x3 = x1 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply nat_p_omega with
0.
The subproof is completed by applying nat_0.
Apply unknownprop_4ab72f93767fc325730724758d3093e7af2a82217c4d5ee8a2692818e418bf07 with
x0,
x1,
λ x2 x3 . K_field_2_b x0 x0 x1 x3 = x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_ec3d3d5378c24600f44cfd46dcc625e687044d4b8014b4d6229529959afb3fb4 with
x0,
x1,
K_field_4 x0 x0,
λ x2 x3 . x3 = x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_1a3d25fd41b7c3c508a2fe54709eb7f884df8973d52168382e0bc01da2bfd1d5 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_6790bfb1084e54a662599ffbd2a505ea724706951dc535759f7c4c6075e28526 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.