Library ZFind_basic

Require Import ZF ZFnats.


Definition UNIT := succ zero.
Lemma unit_typ : zero ∈ UNIT.

Lemma unit_elim : ∀ p, p ∈ UNIT -> p == zero.

Definition BOOL := succ (succ zero).
Definition TRUE := zero.
Definition FALSE := succ zero.

Lemma true_typ : TRUE ∈ BOOL.

Lemma false_typ : FALSE ∈ BOOL.

Lemma bool_elim : ∀ b, b ∈ BOOL -> b == TRUE \/ b == FALSE.

Definition EQ A x y :=
  cond_set (x ∈ A /\ x == y) (singl empty).

Instance EQ_morph : Proper (eq_set ==> eq_set ==> eq_set ==> eq_set) EQ.
Qed.

Definition REFL := empty.

Lemma refl_typ : ∀ A x, x ∈ A -> REFL ∈ EQ A x x.

Lemma EQ_elim : ∀ A x y p,
  p ∈ EQ A x y -> x ∈ A /\ x == y /\ p == REFL.

Lemma EQ_ind : ∀ A P,
  Proper (eq_set ==> eq_set ==> iff) P ->
  ∀ x y p, P x REFL -> p ∈ EQ A x y -> P y p.