---

Step * of Lemma spread-axiom-sqequal-bottom

∀[F:Top]. (let a,b = Ax in F[a;b] ~ ⊥)
BY
{ ((RWO "stuck-spread" 0 THEN Auto) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F:Top].  (let  a,b  =  Ax  in  F[a;b]  \msim{}  \mbot{})


By

---

Latex:
((RWO  "stuck-spread"  0  THEN  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index