Let x0 of type ι be given.
Apply finite_ind with
λ x1 . finite (binunion x0 x1) leaving 2 subgoals.
Apply binunion_idr with
x0,
λ x1 x2 . finite x2.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply binunion_asso with
x0,
x1,
Sing x2,
λ x3 x4 . finite x4.
Apply adjoin_finite with
binunion x0 x1,
x2.
The subproof is completed by applying H3.