Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0:
∀ x2 . x2 ∈ x0 ⟶ nIn x2 x1.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with
5 leaving 2 subgoals.
The subproof is completed by applying nat_5.
Apply atleastp_tra with
6,
binunion x0 x1,
5 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply atleastp_tra with
binunion x0 x1,
setsum 1 (prim4 2),
5 leaving 2 subgoals.
Apply unknownprop_94b237fc7b7d3bf1a0a078f7d057802d281bf3c46c36fd56a85d339ac0f07170 with
x0,
x1,
1,
prim4 2 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H0.
Apply equip_atleastp with
setsum 1 (prim4 2),
5.
Apply equip_sym with
5,
setsum 1 (prim4 2).
The subproof is completed by applying unknownprop_df367236b04025a8bc475bb0339f30914d7857f44d1c25f727210d578b124584.