| λ x0 x1 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . and (and (and (Church10_forall (λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x0 x2 Church10_0 = x2)) (Church10_forall2_lt (λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x0 x2 x3 = x0 x3 x2))) (Church10_forall (λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church10_forall (λ x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x0 (x1 x2 x3) x3 = x2)))) (Church10_forall (λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church10_forall (λ x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 (x0 x2 x3) x3 = x2))) |
|