Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
x1,
x0,
λ x3 x4 . x4 = bc82c.. x1 x2 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
x1,
x2,
λ x3 x4 . bc82c.. x0 x1 = x4 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_dff6e8fda85df9e92da1fa7de32e7db4e93608d23c35200508d6d4985bb05bac with
x1,
x0,
x2 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying L4.