Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_b30a94f49240f0717f4ecb200a605aa8a4e6dad6dc5d1afa60c37866ee96baab with
x2,
x0.
Apply notE with
In x2 x1 leaving 2 subgoals.
Apply unknownprop_9bccc16873f624a3c3c071d170820d76e64a5491b15f0c2f0287b0026ecb19b8 with
x2,
x1.
The subproof is completed by applying H1.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.