Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_d018bd0ff7e1673bb0aea059ead181f579bde1ee59189802e506bc50bc706f38 with
616bf.. x0 x1,
x2,
λ x3 x4 . x4 = 616bf.. (14149.. x0 x2) (14149.. x1 x2) leaving 3 subgoals.
Apply unknownprop_6ea59642454c806d36d2cfe931420377c027fcaf6c044cc84fb5291b346de8a0 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_d018bd0ff7e1673bb0aea059ead181f579bde1ee59189802e506bc50bc706f38 with
x0,
x2,
λ x3 x4 . 14149.. x2 (616bf.. x0 x1) = 616bf.. x4 (14149.. x1 x2) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_d018bd0ff7e1673bb0aea059ead181f579bde1ee59189802e506bc50bc706f38 with
x1,
x2,
λ x3 x4 . 14149.. x2 (616bf.. x0 x1) = 616bf.. (14149.. x2 x0) x4 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_f3c9cd006b0ca49dbaea87eee344eae5f575e10742b8882573411ba536c6d868 with
x2,
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
The subproof is completed by applying H1.