Apply add_nat_add_SNo with
2,
2,
λ x0 x1 . x0 = 4 leaving 3 subgoals.
Apply nat_p_omega with
2.
The subproof is completed by applying nat_2.
Apply nat_p_omega with
2.
The subproof is completed by applying nat_2.
The subproof is completed by applying unknownprop_a056e7e1d4164d24a60c8047a73979083395e5609e36aaee67608ba08eded8a1.