Apply unknownprop_f04ee3f2db7dade92ee7be101bff40fb89f733bb0c0340f09b616cd72154ad93 with
λ x0 . e6316.. x0 (4ae4a.. 4a7ef..) = x0.
Let x0 of type ι be given.
Apply unknownprop_0bba6b6e1ff88cb6fe93e4b3f72d170fee2180507070ff2fab0f5b4dc92e6b37 with
x0,
4ae4a.. 4a7ef..,
e6316.. x0 (4ae4a.. 4a7ef..) = x0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_3d71b8748f06c73392acc73d46c8ae7fc07e5709a18169240b1cb765b8547148.
Let x1 of type ι be given.
Let x2 of type ι be given.