---

Step * of Lemma isinl-implies-not-isatom

∀[t:Base]. (¬↑isatom(t)) supposing ((↑isinl(t)) and (t)↓)
BY
{ (CanonicalAuto
   THEN (Assert ⌜↑isatom(t)⌝⋅ THENA Auto)
   THEN MoveToConcl (-3)
   THEN CanonicalAuto
   THEN HypSubst (-1) (-2)
   THEN Reduce (-2)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[t:Base].  (\mneg{}\muparrow{}isatom(t))  supposing  ((\muparrow{}isinl(t))  and  (t)\mdownarrow{})


By

---

Latex:
(CanonicalAuto
  THEN  (Assert  \mkleeneopen{}\muparrow{}isatom(t)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-3)
  THEN  CanonicalAuto
  THEN  HypSubst  (-1)  (-2)
  THEN  Reduce  (-2)
  THEN  Trivial)

---

Home Index