Let x0 of type ι be given.
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
e4431.. x0.
The subproof is completed by applying L2.
Apply unknownprop_a01a97b657898ff9d288e2af990470253bea0ca012cb491bf0a3063b2cc95ddb with
e4431.. x0,
x0 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with
e4431.. x0.
Apply unknownprop_144f26d28c36e53fd447ba70115cd55d32e895160d4fb202367d3cd577066d73 with
x0,
e4431.. x0,
e4431.. x0 = x0 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Apply FalseE with
e4431.. x0 = x0.
Apply unknownprop_334a5a4dfd5441f12538cd3c70458238b05308c372afbd4cf94b09dd8e7afe85 with
x0,
e4431.. x0,
False leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
The subproof is completed by applying H5.
Let x1 of type ι be given.
Apply unknownprop_86d1ac064e08bd36bc8f8c7d3070ea65b389686b3ca603e510b47119b9d626ec with
x1.
Apply unknownprop_fb545b225a42993d98e0d062b6c9208b8321e87814f4e26de3418c134068c2c8 with
x1,
x0,
x1 leaving 5 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
Apply H1 with
x1.
Apply unknownprop_5a5c48612170d465714265799d25003db15da4f2d5d05eaf9fa403276d7d9f0a with
e4431.. x0,
x1,
e4431.. x1 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H13.
Apply unknownprop_90012ae02c7e97888ea4d0a930b01b500b9d0d1d1a0841df69b82a77726b906b with
x1.
The subproof is completed by applying H6.
The subproof is completed by applying H10.
Apply FalseE with
SNoEq_ (e4431.. x0) x0 (e4431.. x0) ⟶ prim1 (e4431.. x0) (e4431.. x0) ⟶ False.
Apply In_irref with
e4431.. x0.
Apply unknownprop_b0d5c07b58c35dec2d98b8c0aef5865d54317627a7a2b363b61462669e811c57 with
e4431.. x0,
λ x1 x2 . prim1 (e4431.. x0) x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H6.
Let x1 of type ι → ι → ο be given.
The subproof is completed by applying H5 with λ x2 x3 . x1 x3 x2.