Apply explicit_Nats_I with
48ef8..,
4a7ef..,
4ae4a.. leaving 5 subgoals.
The subproof is completed by applying unknownprop_f809b902583dacba413959fe07b21224d4e73a721dc40d1113b446998d75c82c.
The subproof is completed by applying unknownprop_b917ac5fdcfe9362f85d63a8724e8017dbbe7778e330739d2360ff28ec54307c.
Let x0 of type ι be given.
The subproof is completed by applying unknownprop_2602cf2bdb1e417af7ff1134e4c9ee68b103b598c85667d3a4d01fe3c406ee63 with x0.
Let x0 of type ι be given.
Let x1 of type ι be given.
The subproof is completed by applying unknownprop_684cb1205e38822a7a824f8a0440cb0f546e66d657860b857331eee8a38df013 with x0, x1.
Let x0 of type ι → ο be given.
Assume H1:
∀ x1 . x0 x1 ⟶ x0 (4ae4a.. x1).
Let x1 of type ι be given.
Apply unknownprop_03f5f7248b8d06fe27b9a4f75f4e437d5e9b43a9092733e8b3f6dcfe61f5e308 with
x1.
The subproof is completed by applying H2.
Apply L3 with
x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.