---

Step * 1 of Lemma btrue_neq_bfalse


1. tt = ff@i
⊢ False
BY
{ ((ApFunToHypEquands `x' if x then 1 else 0 fi  ℤ 1 THENM Reduce (-1)) THEN Auto) }

---

Latex:

---

Latex:

1.  tt  =  ff@i
\mvdash{}  False


By

---

Latex:
((ApFunToHypEquands  `x'  if  x  then  1  else  0  fi    \mBbbZ{}  1  THENM  Reduce  (-1))  THEN  Auto)

---

Home Index