Apply unknownprop_adc51df32e37a02ae01a7627d71f293cbf548824fcf0d70ccbf318430642e27c with
2,
0,
λ x0 x1 . x1 = 2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.
Apply unknownprop_4ef67fc5b8b30ebc0b691020299a978fd97f9ab288d7f37b768f51bf86e2a3c3 with
2,
λ x0 x1 . mul_nat 2 x1 = 2.
The subproof is completed by applying unknownprop_74e06c9344760e4cc873ef5c22b83470d591f1b41a22d02c74881e98d2f21e46 with 2.