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