Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_0016de04f44a712243c9eeee572a992709374894dd4f8741b2a55208a71b7c48 with
x1.
Apply unknownprop_df95567eaac7dcf742571a06351d685ef037c3575a0b273f643efe646824ac1a with
x0,
(λ x2 . SetAdjoin x2 (Sing 1)) x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.