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