Apply unknownprop_eea7f7c01c2f9314c7bc3a085058c480d152ffa7256ea77f85298c177a37d7db with
1,
λ x0 x1 . 0,
λ x0 x1 . 0,
λ x0 x1 . 0,
0 leaving 5 subgoals.
The subproof is completed by applying unknownprop_79681563a76dadf1dbda1046ef47e6de38a75a5961ace6685c10ae38e7dfd830.
The subproof is completed by applying unknownprop_79681563a76dadf1dbda1046ef47e6de38a75a5961ace6685c10ae38e7dfd830.
The subproof is completed by applying unknownprop_79681563a76dadf1dbda1046ef47e6de38a75a5961ace6685c10ae38e7dfd830.
Let x0 of type ι be given.
Apply unknownprop_7f6501f9f8c19f5c2cddf4168679e2ff20a237333cd0d098eed3a3984bc044c0 with
x0,
λ x1 . and ((λ x2 x3 . 0) 0 x1 = x1) ((λ x2 x3 . 0) x1 0 = x1) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
0 = 0,
0 = 0 leaving 2 subgoals.
Let x1 of type ι → ι → ο be given.
Assume H1: x1 0 0.
The subproof is completed by applying H1.
Let x1 of type ι → ι → ο be given.
Assume H1: x1 0 0.
The subproof is completed by applying H1.
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_7f6501f9f8c19f5c2cddf4168679e2ff20a237333cd0d098eed3a3984bc044c0 with
x0,
λ x2 . and (and (and ((λ x3 x4 . 0) x2 ((λ x3 x4 . 0) x2 x1) = x1) ((λ x3 x4 . 0) x2 ((λ x3 x4 . 0) x2 x1) = x1)) ((λ x3 x4 . 0) ((λ x3 x4 . 0) x2 x1) x1 = x2)) ((λ x3 x4 . 0) ((λ x3 x4 . 0) x2 x1) x1 = x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_7f6501f9f8c19f5c2cddf4168679e2ff20a237333cd0d098eed3a3984bc044c0 with
x1,
λ x2 . and (and (and ((λ x3 x4 . 0) 0 ((λ x3 x4 . 0) 0 x2) = x2) ((λ x3 x4 . 0) 0 ((λ x3 x4 . 0) 0 x2) = x2)) ((λ x3 x4 . 0) ((λ x3 x4 . 0) 0 x2) x2 = 0)) ((λ x3 x4 . 0) ((λ x3 x4 . 0) 0 x2) x2 = 0) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_2ff49f839bae019f05670904cb0de7c4d3a370e9709840e618f2b8f87220915c with
0 = 0,
0 = 0,
0 = 0,
0 = 0 leaving 4 subgoals.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 0 0.
The subproof is completed by applying H2.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 0 0.
The subproof is completed by applying H2.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 0 0.
The subproof is completed by applying H2.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 0 0.
The subproof is completed by applying H2.