Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_144f26d28c36e53fd447ba70115cd55d32e895160d4fb202367d3cd577066d73 with
x0,
x1,
fe4bb.. (f4dc0.. x1) (f4dc0.. x0) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_3bb88212dd853920577537bc3ecbc5e3e2bf8309e1e59246b79ae30400fc333e with
f4dc0.. x1,
f4dc0.. x0.
Apply unknownprop_3cc82c9758d3882690e6647e4154486613d1a5c615c0651627364410273ab026 with
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Assume H3: x0 = x1.
Apply H3 with
λ x2 x3 . fe4bb.. (f4dc0.. x1) (f4dc0.. x3).
The subproof is completed by applying unknownprop_f017f6ee910dd235f4bf08afbbbf148d42e1360d8b1094fb435baedbfe8b2ac8 with
f4dc0.. x1.