Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ο be given.
Apply famunionE_impred with
x0,
λ x5 . {div_SNo (add_SNo x2 (mul_SNo x5 x6)) (add_SNo x5 x6)|x6 ∈ x1,SNoLt 0 (add_SNo x5 x6)},
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x5 of type ι be given.
Assume H2: x5 ∈ x0.
Apply ReplSepE_impred with
x1,
λ x6 . SNoLt 0 (add_SNo x5 x6),
λ x6 . div_SNo (add_SNo x2 (mul_SNo x5 x6)) (add_SNo x5 x6),
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply H1 with
x5.
The subproof is completed by applying H2.