---

Step * 1 of Lemma equipollent-two


1. a1 : 𝔹
2. a2 : 𝔹
3. if a1 then 1 else 0 fi  = if a2 then 1 else 0 fi  ∈ ℕ2
⊢ a1 = a2
BY
{ (MoveToConcl (-1) THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

Latex:

1.  a1  :  \mBbbB{}
2.  a2  :  \mBbbB{}
3.  if  a1  then  1  else  0  fi    =  if  a2  then  1  else  0  fi 
\mvdash{}  a1  =  a2


By

---

Latex:
(MoveToConcl  (-1)  THEN  RepeatFor  2  (AutoSplit))

---

Home Index