| Loop = λ x1 . λ x2 x3 x4 : ι → ι → ι . λ x5 . and (and (and (and (binop_on x1 x2) (binop_on x1 x3)) (binop_on x1 x4)) (∀ x6 . In x6 x1 ⟶ and (x2 x5 x6 = x6) (x2 x6 x5 = x6))) (∀ x6 . In x6 x1 ⟶ ∀ x7 . In x7 x1 ⟶ and (and (and (x3 x6 (x2 x6 x7) = x7) (x2 x6 (x3 x6 x7) = x7)) (x4 (x2 x6 x7) x7 = x6)) (x2 (x4 x6 x7) x7 = x6)) |
|