non associative with precedence 90
for @{'false}.
-lemma ex2_1_commute: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
-#A0 #P0 #P1 * /2 width=3/
-qed.
-
(* relations *)
definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
definition confluent: ∀A. predicate (relation A) ≝ λA,R.
∀a0. confluent1 … R a0.
+(* booleans *)
+
+definition is_false: predicate bool ≝ λb.
+ false = b.
+
(* arithmetics *)
lemma lt_refl_false: ∀n. n < n → ⊥.