Let x0 of type ι → ο be given.
Let x1 of type ι be given.
Apply H3 with
λ x2 . and (74e69.. x2) (x0 x2) leaving 3 subgoals.
Apply andI with
74e69.. 5e331..,
x0 5e331.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_2889540f2161c9537dc388d6c2702e3891e2b8722a023eec016fa2e08ac47609.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply H4 with
(λ x4 . and (74e69.. x4) (x0 x4)) (a3eb9.. x2 x3).
Assume H7: x0 x2.
Apply H5 with
(λ x4 . and (74e69.. x4) (x0 x4)) (a3eb9.. x2 x3).
Assume H9: x0 x3.
Apply andI with
74e69.. (a3eb9.. x2 x3),
x0 (a3eb9.. x2 x3) leaving 2 subgoals.
Apply unknownprop_7b384c9f4f31c662ca4b7cd8d8994d6b48c2b0c98a439c0ee694578d2722b3a7 with
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
Apply H1 with
x2,
x3 leaving 4 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply H4 with
(λ x4 . and (74e69.. x4) (x0 x4)) (bf68c.. x2 x3).
Assume H7: x0 x2.
Apply H5 with
(λ x4 . and (74e69.. x4) (x0 x4)) (bf68c.. x2 x3).
Assume H9: x0 x3.
Apply andI with
74e69.. (bf68c.. x2 x3),
x0 (bf68c.. x2 x3) leaving 2 subgoals.
Apply unknownprop_842c4d383b4cb0f3fad8afe2051751f01573f68067c5dbbab8dff7a8e8a060cf with
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
Apply H2 with
x2,
x3 leaving 4 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Apply L4 with
x0 x1.
Assume H6: x0 x1.
The subproof is completed by applying H6.