Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_bad5adbbba30ab6e9c584ed350d824b3c3bff74e61c0a5380ac75f32855c37ee with
x0,
λ x2 x3 . Subq x2 (add_nat x0 x1).
Apply unknownprop_ced5c14ac643c8a50a5e307d612d5bf57f5a5f18e947e825398ee5fec940398b with
x0,
0,
x1 leaving 4 subgoals.
The subproof is completed by applying H0.
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.