| pf |
|---|
Apply add_nat_SL with u12, u4, λ x0 x1 . x1 = u17 leaving 3 subgoals.
The subproof is completed by applying nat_12.
The subproof is completed by applying nat_4.
Apply add_nat_SR with u12, u4, λ x0 x1 . x0 = u17 leaving 2 subgoals.
The subproof is completed by applying nat_4.
The subproof is completed by applying unknownprop_abc20638bf748af1a36f43157efbc918ef01c9604b8bdbaf812a69e5e78ab11d.
■ |
|