Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι be given.
Assume H0:
∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3.
Apply unknownprop_59be5eee144fb0f12156456c7f9888c3f0525fea126d0d8cdf71e5c53005d86a with
1ad11.. x0 (91630.. 4a7ef..),
x1,
x2.
Let x3 of type ι be given.
Apply H0 with
x3.
Apply unknownprop_f3a4771d3d9a8514b2ad16b328a764b0ce93421ae4df5a6923d3e167d035e33a with
x0,
91630.. 4a7ef..,
x3.
The subproof is completed by applying H1.
Apply In_rec_i_eq with
λ x0 . λ x1 : ι → ι . 94f9e.. (1ad11.. x0 (91630.. 4a7ef..)) (λ x2 . x1 x2).
The subproof is completed by applying L0.