Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_df54193808dbf362a1639247261ed5d96fbe79793df63d3adf7cbfabe00d07b2 with
x0,
λ x2 x3 . Subq x2 (add_nat x1 x0) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_6e5a11d05d85f4b7df7fc96ea27485689351f9a7d64e0743959f30286853327c with
0,
x1,
x0 leaving 4 subgoals.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.
The subproof is completed by applying H1.
The subproof is completed by applying unknownprop_48b433c7921d49bb7e4205d5d86f68a84030c1b7df98f7a59f08a308cb665298 with x1.
The subproof is completed by applying H0.