Let x0 of type ι be given.
Let x1 of type ι be given.
Apply H0 with
λ x2 x3 . In x0 x2.
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with x0.
Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with
x1,
x0,
x0 = x1 leaving 3 subgoals.
The subproof is completed by applying L1.
Apply H0 with
λ x2 x3 . In x1 x3.
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with x1.
Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with
x0,
x1,
x0 = x1 leaving 3 subgoals.
The subproof is completed by applying L3.
Apply FalseE with
x0 = x1.
Apply unknownprop_7aafb642c31e9be85457ec0eb47aa596cd38ae4297ed5252dc50af56ee6c9208 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Assume H4: x1 = x0.
Apply unknownprop_cf6cb9ac2ba2b95572013c10cbd74c677c393380327c9f33d6487f09608dd39e with
x1,
x0.
The subproof is completed by applying H4.
Assume H2: x0 = x1.
The subproof is completed by applying H2.