Let x0 of type ι be given.
Let x1 of type ι be given.
Apply xm with
x1 ∈ x0,
False leaving 2 subgoals.
Assume H2: x1 ∈ x0.
Apply H0.
Apply unknownprop_20fce6fc7f2e036c1229cbf996632439eddb19cfae541105a83e5be9c65bc111 with
x0,
x1,
λ x2 x3 . finite x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply binunion_finite with
setminus x0 (Sing x1),
Sing x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying unknownprop_f7016afae9c8976834aae8fd87dfbc66905d8d8b02412954fb76543365d9f363 with x1.
Apply H0.
Apply set_ext with
x0,
setminus x0 (Sing x1),
λ x2 x3 . finite x3 leaving 3 subgoals.
Let x2 of type ι be given.
Assume H3: x2 ∈ x0.
Apply setminusI with
x0,
Sing x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply H2.
Apply SingE with
x1,
x2,
λ x3 x4 . x3 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H3.
The subproof is completed by applying setminus_Subq with
x0,
Sing x1.
The subproof is completed by applying H1.