---

Step * of Lemma atom-implies-ispair-right

∀[b,c:Top]. ∀[a:Atom].  (if a is a pair then b otherwise c ~ c)
BY
{ (Auto
   THEN SqEqualTopToBase
   THEN HVimplies 0 [1]
   THEN (Assert ⌜False⌝⋅ THEN Auto)
   THEN (Assert ⌜isatom(a) ~ tt⌝⋅ THENA (Reduce 0 THEN Auto))
   THEN HypSubst (-2) (-1)
   THEN Reduce (-1)
   THEN InstLemma `not-btrue-sqeq-bfalse` []
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[b,c:Top].  \mforall{}[a:Atom].    (if  a  is  a  pair  then  b  otherwise  c  \msim{}  c)


By

---

Latex:
(Auto
  THEN  SqEqualTopToBase
  THEN  HVimplies  0  [1]
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (Assert  \mkleeneopen{}isatom(a)  \msim{}  tt\mkleeneclose{}\mcdot{}  THENA  (Reduce  0  THEN  Auto))
  THEN  HypSubst  (-2)  (-1)
  THEN  Reduce  (-1)
  THEN  InstLemma  `not-btrue-sqeq-bfalse`  []
  THEN  Auto)

---

Home Index