Let x0 of type ι be given.
Apply H0 with
79148.. x0.
Apply andI with
x0 ∈ int,
divides_int 2 x0 leaving 2 subgoals.
Apply Subq_omega_int with
x0.
The subproof is completed by applying H1.
Apply divides_nat_divides_int with
2,
x0.
Apply unknownprop_08fb078d795c0975d950898a1224977eb8db97682ff225342ef66a3071181f64 with
x0.
The subproof is completed by applying H0.