Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_0aeb103bb8c1020fd1bbf8133fbf92076b19ca29b614a77dbfc670876f391329 with
236dc.. x0 x1,
ce322.. (236dc.. x0 x1) = x0 leaving 2 subgoals.
Apply unknownprop_a11dfa210cd480918339ec3ee480411b7f4945c0aeef474c01ca879d15816c74 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply H3 with
ce322.. (236dc.. x0 x1) = x0.
Let x2 of type ι be given.
Apply H4 with
ce322.. (236dc.. x0 x1) = x0.
Let x3 of type ι → ι → ο be given.
Apply unknownprop_20aee288fe544593cb730f361570be2fc95d6b53d7a983cf10cd18dc24e2d96a with
x0,
x1,
ce322.. (236dc.. x0 x1),
x2,
λ x4 x5 . x3 x5 x4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H6.