Let x0 of type ι be given.
Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with
Sing x0,
1,
λ x1 . 0.
Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with
Sing x0,
1,
λ x1 . 0 leaving 2 subgoals.
Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with
Sing x0,
1,
λ x1 . 0 leaving 2 subgoals.
Let x1 of type ι be given.
The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H2: (λ x3 . 0) x1 = (λ x3 . 0) x2.
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
x0,
x2,
λ x3 x4 . x1 = x4 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
x0,
x1.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Let x2 of type ο be given.
Assume H1:
∀ x3 . and (In x3 (Sing x0)) (0 = x1) ⟶ x2.
Apply H1 with
x0.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
In x0 (Sing x0),
0 = x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_e96dbc98c3bbaccd959c44021711d14fb0c42be8979571d40cfb87c8bcb73964 with x0.
Apply unknownprop_7f6501f9f8c19f5c2cddf4168679e2ff20a237333cd0d098eed3a3984bc044c0 with
x1,
λ x3 . 0 = x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι → ι → ο be given.
Assume H2: x3 0 0.
The subproof is completed by applying H2.