Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_3069c6fa8dbd033f1c94555c93d580ac5c2fd979807cb20dbdb8dc4cc9b1517f with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_0bc05861c326df1bc856e9663c3bd091fe6729155095d255366b172bf07600be with
x2,
x1,
λ x3 x4 . In x4 (add_nat x2 x0) leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying L3.
Apply unknownprop_0bc05861c326df1bc856e9663c3bd091fe6729155095d255366b172bf07600be with
x2,
x0,
λ x3 x4 . In (add_nat x1 x2) x4 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
Apply unknownprop_4091ebd6d94cd2a61820d5e9e5b329a35ceeb943e078c5c25a4c8d631106573d with
x0,
x1,
x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.