Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_4db127623a54dea607d4178c4cffe8099fa715d4dd5c11459d1bd4ea367db087 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_4db127623a54dea607d4178c4cffe8099fa715d4dd5c11459d1bd4ea367db087 with
x1.
The subproof is completed by applying H1.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
In x0 x1,
Subq x1 x0,
Subq (add_nat x0 x2) (add_nat x1 x2) leaving 3 subgoals.
Apply unknownprop_682983ef060476485fcd03b6da6255e287c5314c9013030e2a8b79c1fa302a8c with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
Apply unknownprop_3336121954edce0fefb5edee2ad1b426a9827aac09625122db0ff807b493dc73 with
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Apply unknownprop_92b4103b83752522eb6c235601eefa2912e3f6395a346e3a7eb52bb5e37ede81 with
add_nat x1 x2,
add_nat x0 x2 leaving 2 subgoals.
The subproof is completed by applying L7.
Apply unknownprop_4091ebd6d94cd2a61820d5e9e5b329a35ceeb943e078c5c25a4c8d631106573d with
x1,
x0,
x2 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H6.
The subproof is completed by applying H3.
Claim L7: x0 = x1
Apply unknownprop_a23ec6a55ac212526d74cbf0d04096929ad453b0eb0f8023e32b8a33930d39fb with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
Apply L7 with
λ x3 x4 . Subq (add_nat x4 x2) (add_nat x1 x2).
The subproof is completed by applying unknownprop_d889823a5c975ad2d68f484964233a1e69e7d67f0888aa5b83d962eeca107acd with
add_nat x1 x2.