Apply unknownprop_dff6e8fda85df9e92da1fa7de32e7db4e93608d23c35200508d6d4985bb05bac with
4a7ef..,
f4dc0.. 4a7ef..,
4a7ef.. leaving 4 subgoals.
The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.
Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with
4a7ef...
The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.
The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.
Claim L0: ∀ x2 : ι → ο . x2 y1 ⟶ x2 y0
Let x2 of type ι → ο be given.
Apply unknownprop_5cbe8643f1e45151334fcd7208ed4c5dc2b120486b5022cdc81170c910647c5d with
4a7ef..,
λ x3 . x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.
set y3 to be λ x3 . x2
Apply unknownprop_ccff4249496414413c3c95467fb8c02c96509ca2826dc03833e7de26e75fcd74 with
4a7ef..,
λ x4 x5 . y3 x5 x4 leaving 2 subgoals.
The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.
The subproof is completed by applying H0.
Let x2 of type ι → ι → ο be given.
Apply L0 with
λ x3 . x2 x3 y1 ⟶ x2 y1 x3.
Assume H1: x2 y1 y1.
The subproof is completed by applying H1.