Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Let x3 of type ι → ι be given.
Assume H1:
∀ x4 . prim1 x4 x0 ⟶ Subq (x2 x4) (x3 x4).
Let x4 of type ι be given.
Apply and3E with
aae7a.. (e76d4.. x4) (22ca9.. x4) = x4,
prim1 (e76d4.. x4) x0,
prim1 (22ca9.. x4) (x2 (e76d4.. x4)),
prim1 x4 (0fc90.. x1 x3) leaving 2 subgoals.
Apply unknownprop_4861fab3b9bde4ccc5c91f323e4d2535c7d435027e9067e34ce3781cfa602d01 with
x0,
x2,
x4.
The subproof is completed by applying H2.
Apply H3 with
λ x5 x6 . prim1 x5 (0fc90.. x1 (λ x7 . x3 x7)).
Apply unknownprop_1f27075d0cd8d16888a609d68ca6246fb2307839dccadd646f85ab18bdcaae8e with
x1,
x3,
e76d4.. x4,
22ca9.. x4 leaving 2 subgoals.
Apply H0 with
e76d4.. x4.
The subproof is completed by applying H4.
Apply H1 with
e76d4.. x4,
22ca9.. x4 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.