Apply unknownprop_adc51df32e37a02ae01a7627d71f293cbf548824fcf0d70ccbf318430642e27c with
2,
1,
λ x0 x1 . x1 = 4 leaving 2 subgoals.
The subproof is completed by applying unknownprop_8d353ccfb170ea018406af7266d499508cf5be2cebcac5c8a89ccd16a50d0251.
Apply unknownprop_f1b4b3f3609f7bbf0bc8735b08d44bfebb6a6346e99882a47fb54ee009e3ab08 with
λ x0 x1 . mul_nat 2 x1 = 4.
The subproof is completed by applying unknownprop_fc29333ca215875c59d1d4fec7fe055141fc81ca507ff0a8a9aa6809347a18a7.