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