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.
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.