Let x0 of type ι be given.
Apply unknownprop_85336ee07ace71a942dc508d3b8c851d9d6bb88511443b7dafbf11b71c263f4d with
λ x1 . 616bf.. x0 x1 = 616bf.. x1 x0 leaving 2 subgoals.
Apply unknownprop_8c15e13006123b2ecc8638fc7a608f34894921ffab471c568a86943fc48f66b4 with
x0,
λ x1 x2 . 616bf.. x0 4a7ef.. = x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_0d2e8618ea244d22f7cc913b00fa77b277d9ba7cc6a18877e00000ded7fa2c79 with x0.
Let x1 of type ι be given.
Apply unknownprop_e235f8bae1d60ca9fa526cccc0fa6abba94ef7e4bc8a87e3104c92958237f126 with
x1,
x0,
λ x2 x3 . 616bf.. x0 (4ae4a.. x1) = x3 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply H2 with
λ x2 x3 . 616bf.. x0 (4ae4a.. x1) = 4ae4a.. x2.
Apply unknownprop_52ad2c641f06ccb05422449032c6daa178243ae05b1152998946ffec9f2dc331 with
x0,
x1.
The subproof is completed by applying H1.