∀ x0 x1 x2 x3 . In x0 4 ⟶ In x1 4 ⟶ In x2 4 ⟶ In x3 4 ⟶ not (x0 = x1) ⟶ not (x0 = x2) ⟶ not (x0 = x3) ⟶ not (x1 = x2) ⟶ not (x1 = x3) ⟶ not (x2 = x3) ⟶ bij 4 4 (ap (lam 4 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 (If_i (x4 = 2) x2 x3))))) |
|