Apply Inj1_setsum_1L with
prim4 2,
λ x0 x1 . equip 5 x1.
Apply unknownprop_c0c4d5a2bc2380a9bf5f072ca1b6c6de0f9cf249a6300964520a8eca88f1ad2a with
4,
prim4 2.
The subproof is completed by applying unknownprop_a2e75caeebe46359eec4abf3d977b407a386725b84f4aeac6b92aa7fc83ac4b8.