Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_4952cbeaa3cfbe39042137e565a281ffc28405c7de4fe454358dcf1400b68a14 with
2,
b97a8.. x0 x1 x2 x3.
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply unknownprop_ba6d0de3ea1c2beeca9d6a57f630aeac271753c66312f1f2e9496df2b38ad2c6 with
x4,
λ x6 . In (b97a8.. x0 x1 x2 x3 x6 x5) 2 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_ba6d0de3ea1c2beeca9d6a57f630aeac271753c66312f1f2e9496df2b38ad2c6 with
x5,
λ x6 . In (b97a8.. x0 x1 x2 x3 0 x6) 2 leaving 3 subgoals.
The subproof is completed by applying H5.
Apply unknownprop_9c43f08812b4dd12e16f83d97b657d94c742c61c9c96af9dabc40f61e694ba78 with
x0,
x1,
x2,
x3,
λ x6 x7 . In x7 2.
The subproof is completed by applying H0.
Apply unknownprop_f07ae9127bc708c3632ef1a3da3981ff971ea451f474f8c231ad0c3fc5f499f5 with
x0,
x1,
x2,
x3,
λ x6 x7 . In x7 2.
The subproof is completed by applying H1.
Apply unknownprop_ba6d0de3ea1c2beeca9d6a57f630aeac271753c66312f1f2e9496df2b38ad2c6 with
x5,
λ x6 . In (b97a8.. x0 x1 x2 x3 1 x6) 2 leaving 3 subgoals.
The subproof is completed by applying H5.
Apply unknownprop_7aef1141b9598ddc8d44b7c4c3b483f1f0f6c18a26ff20a05eb1620b1cbe4c8d with
x0,
x1,
x2,
x3,
λ x6 x7 . In x7 2.
The subproof is completed by applying H2.
Apply unknownprop_90a04ec34931ff614f43f95dd0748ea45c65fd2bd224a57a8c6ddfc9ada05b60 with
x0,
x1,
x2,
x3,
λ x6 x7 . In x7 2.
The subproof is completed by applying H3.