Apply unknownprop_3defe724d02ba276d9730f9f5a87e86e6bc0e48da350a99bdaaf13f339867dcf with
2,
1,
λ x0 x1 . x1 = 4 leaving 2 subgoals.
The subproof is completed by applying unknownprop_8d353ccfb170ea018406af7266d499508cf5be2cebcac5c8a89ccd16a50d0251.
Apply unknownprop_74e06c9344760e4cc873ef5c22b83470d591f1b41a22d02c74881e98d2f21e46 with
2,
λ x0 x1 . add_nat 2 x1 = 4.
The subproof is completed by applying unknownprop_73c08fd5307f656249c9bc1b76ac9a0b21c5e7a3f5a4e3dad32d46dffb7bc549 with 2.