Apply unknownprop_a056e7e1d4164d24a60c8047a73979083395e5609e36aaee67608ba08eded8a1 with
λ x0 x1 . equip x0 (setsum 2 2).
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with
2,
2,
2,
2 leaving 4 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying nat_2.
The subproof is completed by applying equip_ref with 2.
The subproof is completed by applying equip_ref with 2.