Let x0 of type ι → ι be given.
Let x1 of type ι be given.
Apply unknownprop_7286e98d609aa746e0fd442fb25d48ecc298d66ff863c06370951cf0a76dad5e with
λ x2 x3 : ι → ι . Repl (x3 x1) (λ x4 . x0 x4) = x3 (x0 x1).
The subproof is completed by applying unknownprop_d7492b2bd25f96a29674e5cbccec59e3616bffb65459f3cd83d96ccc3a1aa182 with x0, x1, x1.