Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_6df04587a59e9b54f0549c96144213d94328d0b365474f739b895e743839c817 with
x0,
x2,
λ x3 x4 . x4 = add_CSNo x1 x2 ⟶ x0 = x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_6df04587a59e9b54f0549c96144213d94328d0b365474f739b895e743839c817 with
x1,
x2,
λ x3 x4 . add_CSNo x2 x0 = x4 ⟶ x0 = x1 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_06a4ec1d06df31c2c8c53ecdf2780bb9f187c1468b28741ccdfd338035b0de7f 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.