Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ο be given.
Let x3 of type ι → ο be given.
Let x4 of type ι → ο be given.
Apply H3 with
or (40dde.. x0 x2 x1 x4) (and (x0 = x1) (PNoEq_ x0 x2 x4)) leaving 2 subgoals.
Apply orIL with
40dde.. x0 x2 x1 x4,
and (x0 = x1) (PNoEq_ x0 x2 x4).
Apply unknownprop_516ec77a0547bdde87f302357c77a8c500e4737d03bed523bd783f1c87c1572b with
x0,
x1,
x2,
x3,
x4 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Apply H4 with
or (40dde.. x0 x2 x1 x4) (and (x0 = x1) (PNoEq_ x0 x2 x4)).
Assume H5: x0 = x1.
Apply orIR with
40dde.. x0 x2 x1 x4,
and (x0 = x1) (PNoEq_ x0 x2 x4).
Apply andI with
x0 = x1,
PNoEq_ x0 x2 x4 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply PNoEq_tra_ with
x0,
x2,
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H6.