---

Definition: bool
𝔹 ==  Unit?

Lemma: bool_wf
𝔹 ∈ Type

Definition: btrue
tt ==  inl ⋅

Lemma: btrue_wf
tt ∈ 𝔹

Definition: bfalse
ff ==  inr ⋅ 

Lemma: bfalse_wf
ff ∈ 𝔹

Lemma: bool_subtype_base
𝔹 ⊆r Base

Lemma: bool_cases_sqequal
∀b:𝔹. ((b ~ tt) ∨ (b ~ ff))

Lemma: bool_cases
∀b:𝔹. (b = tt ∨ b = ff)

Definition: eq_int
(i =z j) ==  if i=j then tt else ff

Lemma: eq_int_wf
∀[i,j:ℤ].  ((i =z j) ∈ 𝔹)

Definition: lt_int
i <z j ==  if (i) < (j)  then tt  else ff

Lemma: lt_int_wf
∀[i,j:ℤ].  (i <z j ∈ 𝔹)

Lemma: member-less_than'
∀[a,b:ℤ].  Ax ∈ less_than'(a;b) supposing less_than'(a;b)

Lemma: member-less_than
∀[a,b:ℤ].  Ax ∈ a < b supposing a < b

Lemma: sq_stable__less_than
∀[a,b:ℤ].  SqStable(a < b)

Definition: eq_atom
x =a y ==  if x=y then tt else ff fi 

Lemma: eq_atom_wf
∀[x,y:Atom].  (x =a y ∈ 𝔹)



Home Index