---

Step * of Lemma unit-mono

mono(Unit)
BY
{ (((D 0 THEN Auto) THEN D 1) THEN FLemma `is-above-axiom` [-1] THEN Auto THEN HypSubst (-1) 0 THEN Auto) }

---

Latex:

---

Latex:
mono(Unit)


By

---

Latex:
(((D  0  THEN  Auto)  THEN  D  1)
  THEN  FLemma  `is-above-axiom`  [-1]
  THEN  Auto
  THEN  HypSubst  (-1)  0
  THEN  Auto)

---

Home Index