Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_144f26d28c36e53fd447ba70115cd55d32e895160d4fb202367d3cd577066d73 with
x1,
x2,
fe4bb.. (bc82c.. x0 x1) (bc82c.. x0 x2) leaving 5 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_3bb88212dd853920577537bc3ecbc5e3e2bf8309e1e59246b79ae30400fc333e with
bc82c.. x0 x1,
bc82c.. x0 x2.
Apply unknownprop_50ea7279d1527aec8642473c7707da12238935f258091dd2df6f6eae075c74e1 with
x0,
x1,
x2 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.
Assume H4: x1 = x2.
Apply H4 with
λ x3 x4 . fe4bb.. (bc82c.. x0 x4) (bc82c.. x0 x2).
The subproof is completed by applying unknownprop_f017f6ee910dd235f4bf08afbbbf148d42e1360d8b1094fb435baedbfe8b2ac8 with
bc82c.. x0 x2.