Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_497ef0b809178e9ac674acf0f41f994a7e76b824de0430efd934f6540a71daab with
x0,
x1,
exactly1of3 (In x0 x1) (x0 = x1) (In x1 x0) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_c72194c7d1f5ce36ad1b0f76e0486dc8be176c356f38465d3b59feea49e50884 with
In x0 x1,
x0 = x1,
In x1 x0 leaving 3 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
x0 = x1.
Assume H3: x0 = x1.
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with
x0,
x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_c08c2271cf6ba0885c1e030cb2abcd9decbf5e7798ef2ffc9064daf191c9f920 with x0.
Apply H3 with
λ x2 x3 . In x0 x3.
The subproof is completed by applying H2.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
In x1 x0.
Apply unknownprop_7aafb642c31e9be85457ec0eb47aa596cd38ae4297ed5252dc50af56ee6c9208 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Assume H2: x0 = x1.
Apply unknownprop_77a7928eabea542e6c3d7d07245e23f57ff87edf3b804c5c9603aea522365120 with
In x0 x1,
x0 = x1,
In x1 x0 leaving 3 subgoals.
Apply unknownprop_6e5a093609fdb2cdfae678bb0b08050c8cb0f957c58eff59fd62e4c9ba5321d5 with
λ x2 x3 : ι → ι → ο . x2 x0 x1.
Apply H2 with
λ x2 x3 . nIn x3 x1.
The subproof is completed by applying unknownprop_c08c2271cf6ba0885c1e030cb2abcd9decbf5e7798ef2ffc9064daf191c9f920 with x1.
The subproof is completed by applying H2.
Apply unknownprop_6e5a093609fdb2cdfae678bb0b08050c8cb0f957c58eff59fd62e4c9ba5321d5 with
λ x2 x3 : ι → ι → ο . x2 x1 x0.
Apply H2 with
λ x2 x3 . nIn x1 x3.
The subproof is completed by applying unknownprop_c08c2271cf6ba0885c1e030cb2abcd9decbf5e7798ef2ffc9064daf191c9f920 with x1.
Apply unknownprop_0e7bb1ce65186698c0e2af57c438b03c7036e5976d61e23ace681558164f440a with
In x0 x1,
x0 = x1,
In x1 x0 leaving 3 subgoals.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
In x0 x1.
Apply unknownprop_7aafb642c31e9be85457ec0eb47aa596cd38ae4297ed5252dc50af56ee6c9208 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
x0 = x1.
Assume H3: x0 = x1.
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with
x0,
x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_c08c2271cf6ba0885c1e030cb2abcd9decbf5e7798ef2ffc9064daf191c9f920 with x0.
Apply H3 with
λ x2 x3 . In x3 x0.
The subproof is completed by applying H2.
The subproof is completed by applying H2.