Let x0 of type ι → (ι → ι) → ι be given.
Assume H0:
∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3.
Let x1 of type ι be given.
Apply unknownprop_089e5753cf2e7dccb3413f7d66a960e8aad6e35cd179a1403ba7d68a788bdf0b with
x0,
x1,
In_rec_poly_i x0 x1,
x0 x1 (In_rec_poly_i x0) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_ea667e8c5984fa10a111dd451427cddccf3b49b0ad2764e849c70aa538387c01 with
x0,
x1.
The subproof is completed by applying H0.
Apply unknownprop_e9796c3bec39bf4a19db7cb47c824e2f215acd68f0c386169ef3ead02b1deffa with
x0,
x1.
The subproof is completed by applying H0.