---

Step * 1 of Lemma biject-bool-nsub2


1. a1 : 𝔹
⊢ ∀a2:𝔹. ((if a1 then 1 else 0 fi  = if a2 then 1 else 0 fi  ∈ ℕ2) ⇒ a1 = a2)
BY
{ ((BoolCase ⌜a1⌝⋅ THENA Auto) THEN (D 0 THENA Auto) THEN BoolCase ⌜a2⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a1  :  \mBbbB{}
\mvdash{}  \mforall{}a2:\mBbbB{}.  ((if  a1  then  1  else  0  fi    =  if  a2  then  1  else  0  fi  )  {}\mRightarrow{}  a1  =  a2)


By

---

Latex:
((BoolCase  \mkleeneopen{}a1\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (D  0  THENA  Auto)  THEN  BoolCase  \mkleeneopen{}a2\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index