Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
In x0 x1,
Subq x1 x0,
or (Subq x0 x1) (Subq x1 x0) leaving 3 subgoals.
Apply unknownprop_682983ef060476485fcd03b6da6255e287c5314c9013030e2a8b79c1fa302a8c with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
Subq x0 x1,
Subq x1 x0.
Apply unknownprop_5d43e074a46031aba9b972e1346a32eab5bc6d7f8cd872222d3a15fe3889dd90 with
λ x2 x3 : ι → ι → ο . x3 x0 x1.
Apply unknownprop_16d203cf35db7c43083950b8cdf3bc14c48faba5d53a8b40d54b8c3e00a23527 with
x1,
x0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with
Subq x0 x1,
Subq x1 x0.
The subproof is completed by applying H2.