Apply unknownprop_eea7f7c01c2f9314c7bc3a085058c480d152ffa7256ea77f85298c177a37d7db with
2,
b97a8.. 0 1 1 0,
b97a8.. 0 1 1 0,
b97a8.. 0 1 1 0,
0 leaving 5 subgoals.
The subproof is completed by applying unknownprop_2657fea9438ca143ef1c3d358da6b7b474d34e0ce53a20a28c895c48c2204fcc.
The subproof is completed by applying unknownprop_2657fea9438ca143ef1c3d358da6b7b474d34e0ce53a20a28c895c48c2204fcc.
The subproof is completed by applying unknownprop_2657fea9438ca143ef1c3d358da6b7b474d34e0ce53a20a28c895c48c2204fcc.
Let x0 of type ι be given.
Apply unknownprop_ba6d0de3ea1c2beeca9d6a57f630aeac271753c66312f1f2e9496df2b38ad2c6 with
x0,
λ x1 . and (b97a8.. 0 1 1 0 0 x1 = x1) (b97a8.. 0 1 1 0 x1 0 = x1) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
b97a8.. 0 1 1 0 0 0 = 0,
b97a8.. 0 1 1 0 0 0 = 0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_9c43f08812b4dd12e16f83d97b657d94c742c61c9c96af9dabc40f61e694ba78 with 0, 1, 1, 0.
The subproof is completed by applying unknownprop_9c43f08812b4dd12e16f83d97b657d94c742c61c9c96af9dabc40f61e694ba78 with 0, 1, 1, 0.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
b97a8.. 0 1 1 0 0 1 = 1,
b97a8.. 0 1 1 0 1 0 = 1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_f07ae9127bc708c3632ef1a3da3981ff971ea451f474f8c231ad0c3fc5f499f5 with 0, 1, 1, 0.
The subproof is completed by applying unknownprop_7aef1141b9598ddc8d44b7c4c3b483f1f0f6c18a26ff20a05eb1620b1cbe4c8d with 0, 1, 1, 0.
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_ba6d0de3ea1c2beeca9d6a57f630aeac271753c66312f1f2e9496df2b38ad2c6 with
x0,
λ x2 . and (and (and (b97a8.. 0 1 1 0 x2 (b97a8.. 0 1 1 0 x2 x1) = x1) (b97a8.. 0 1 1 0 x2 (b97a8.. 0 1 1 0 x2 x1) = x1)) (b97a8.. 0 1 1 0 (b97a8.. 0 1 1 0 x2 x1) x1 = x2)) (b97a8.. 0 1 1 0 (b97a8.. 0 1 1 0 x2 x1) x1 = x2) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_ba6d0de3ea1c2beeca9d6a57f630aeac271753c66312f1f2e9496df2b38ad2c6 with
x1,
λ x2 . and (and (and (b97a8.. 0 1 1 0 0 (b97a8.. 0 1 1 0 0 x2) = x2) (b97a8.. 0 1 1 0 0 (b97a8.. 0 1 1 0 0 x2) = x2)) (b97a8.. 0 1 1 0 (b97a8.. 0 1 1 0 0 x2) x2 = 0)) (b97a8.. 0 1 1 0 (b97a8.. 0 1 1 0 0 x2) x2 = 0) leaving 3 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_2ff49f839bae019f05670904cb0de7c4d3a370e9709840e618f2b8f87220915c with
b97a8.. 0 1 1 0 0 (b97a8.. 0 1 1 0 0 0) = 0,
b97a8.. 0 1 1 0 0 (b97a8.. 0 1 1 0 0 0) = 0,
b97a8.. 0 1 1 0 ... 0 = 0,
... leaving 4 subgoals.