Apply unknownprop_4952cbeaa3cfbe39042137e565a281ffc28405c7de4fe454358dcf1400b68a14 with
Sing 0,
λ x0 x1 . 0.
Let x0 of type ι be given.
Let x1 of type ι be given.
The subproof is completed by applying unknownprop_e96dbc98c3bbaccd959c44021711d14fb0c42be8979571d40cfb87c8bcb73964 with (λ x2 x3 . 0) x0 x1.
Claim L1:
∀ x0 . In x0 (Sing 0) ⟶ 0 = x0Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
0,
x0,
λ x2 x3 . x1 x3 x2.
The subproof is completed by applying H1.
Apply unknownprop_eea7f7c01c2f9314c7bc3a085058c480d152ffa7256ea77f85298c177a37d7db with
Sing 0,
λ x0 x1 . 0,
λ x0 x1 . 0,
λ x0 x1 . 0,
Sing 0 leaving 5 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L0.
The subproof is completed by applying L0.
Let x0 of type ι be given.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
(λ x1 x2 . 0) (Sing 0) x0 = x0,
(λ x1 x2 . 0) x0 (Sing 0) = x0 leaving 2 subgoals.
Apply L1 with
x0.
The subproof is completed by applying H2.
Apply L1 with
x0.
The subproof is completed by applying H2.
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_2ff49f839bae019f05670904cb0de7c4d3a370e9709840e618f2b8f87220915c with
(λ x2 x3 . 0) x0 ((λ x2 x3 . 0) x0 x1) = x1,
(λ x2 x3 . 0) x0 ((λ x2 x3 . 0) x0 x1) = x1,
(λ x2 x3 . 0) ((λ x2 x3 . 0) x0 x1) x1 = x0,
(λ x2 x3 . 0) ((λ x2 x3 . 0) x0 x1) x1 = x0 leaving 4 subgoals.
Apply L1 with
x1.
The subproof is completed by applying H3.
Apply L1 with
x1.
The subproof is completed by applying H3.
Apply L1 with
x0.
The subproof is completed by applying H2.
Apply L1 with
x0.
The subproof is completed by applying H2.