---

Step * of Lemma equipollent-two

𝔹 ~ ℕ2
BY
{ ((With ⌜λb.if b then 1 else 0 fi ⌝ (D 0)⋅ THEN Auto) THEN RepeatFor 2 (D 0) THEN Reduce 0 THEN Auto) }

1
1. a1 : 𝔹
2. a2 : 𝔹
3. if a1 then 1 else 0 fi  = if a2 then 1 else 0 fi  ∈ ℕ2
⊢ a1 = a2

2
1. b : ℕ2
⊢ ∃a:𝔹. (if a then 1 else 0 fi  = b ∈ ℕ2)

---

Latex:

---

Latex:
\mBbbB{}  \msim{}  \mBbbN{}2


By

---

Latex:
((With  \mkleeneopen{}\mlambda{}b.if  b  then  1  else  0  fi  \mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)  THEN  RepeatFor  2  (D  0)  THEN  Reduce  0  THEN  Auto)

---

Home Index