---

Step * 2 of Lemma biject-bool-nsub2


1. b : ℕ2
⊢ ∃a:𝔹. (if a then 1 else 0 fi  = b ∈ ℕ2)
BY
{ ((IntSegCases 1 THENL [D 0 With ⌜ff⌝ ; D 0 With ⌜tt⌝ ]) THEN Auto) }

---

Latex:

---

Latex:

1.  b  :  \mBbbN{}2
\mvdash{}  \mexists{}a:\mBbbB{}.  (if  a  then  1  else  0  fi    =  b)


By

---

Latex:
((IntSegCases  1  THENL  [D  0  With  \mkleeneopen{}ff\mkleeneclose{}  ;  D  0  With  \mkleeneopen{}tt\mkleeneclose{}  ])  THEN  Auto)

---

Home Index