Let x0 of type ι be given.
Apply H1 with
False.
Let x1 of type ι be given.
Apply H2 with
False.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with
x1 leaving 2 subgoals.
Apply omega_nat_p with
x1.
The subproof is completed by applying H3.
Apply atleastp_tra with
ordsucc x1,
x0,
x1 leaving 2 subgoals.
Apply atleastp_tra with
ordsucc x1,
omega,
x0 leaving 2 subgoals.
Apply Subq_atleastp with
ordsucc x1,
omega.
Let x2 of type ι be given.
Apply nat_p_omega with
x2.
Apply nat_p_trans with
ordsucc x1,
x2 leaving 2 subgoals.
Apply nat_ordsucc with
x1.
Apply omega_nat_p with
x1.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying H0.
Apply equip_atleastp with
x0,
x1.
The subproof is completed by applying H4.