---

Step * of Lemma equal_bool_if

∀[a,b:𝔹].  (a = b) supposing ((¬((↑a) ∧ (¬↑b))) and (¬((¬↑a) ∧ (↑b))))
BY
{ (Intros THEN RepeatFor 2 (BoolInd 1) THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbB{}].    (a  =  b)  supposing  ((\mneg{}((\muparrow{}a)  \mwedge{}  (\mneg{}\muparrow{}b)))  and  (\mneg{}((\mneg{}\muparrow{}a)  \mwedge{}  (\muparrow{}b))))


By

---

Latex:
(Intros  THEN  RepeatFor  2  (BoolInd  1)  THEN  All  Reduce  THEN  Auto)

---

Home Index