---

Step * of Lemma pi1-axiom

fst(Ax) ~ ⊥
BY
{ (Unfold `pi1` 0 THEN RWO "spread-axiom-sqequal-bottom" 0 THEN Auto) }

---

Latex:

---

Latex:
fst(Ax)  \msim{}  \mbot{}


By

---

Latex:
(Unfold  `pi1`  0  THEN  RWO  "spread-axiom-sqequal-bottom"  0  THEN  Auto)

---

Home Index