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