Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι be given. Assume H0: nSubq x0 x1 ⟶ False. Apply unknownprop_b777a79c17f16cd28153af063df26a4626b11c1f1d4394d7f537c11837ab0962 with Subq x0 x1. Assume H1: not (Subq x0 x1). Apply H0. Apply unknownprop_604592dc5fe257d05bd9e42fd3eadcbb243b22bec35d240b4b58a45260f0d199 with x0, x1. The subproof is completed by applying H1. ■