---

Step * of Lemma has-value-implies-dec-ispair-2

∀t:Base. ((t)↓ ⇒ ((t ~ <fst(t), snd(t)>) ∨ (∀a,b:Base.  (if t is a pair then a otherwise b ~ b))))
BY
{ (Auto
   THEN InstLemma `has-value-implies-dec-ispair` [⌜t⌝;⌜0⌝;⌜1⌝]⋅
   THEN Auto
   THEN ParallelLast
   THEN Auto
   THEN CanonicalTestCases
   THEN Auto
   THEN HypSubst (-1) (-4)
   THEN Reduce (-4)
   THEN FLemma `not_zero_sqequal_one` [-4]
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}t:Base.  ((t)\mdownarrow{}  {}\mRightarrow{}  ((t  \msim{}  <fst(t),  snd(t)>)  \mvee{}  (\mforall{}a,b:Base.    (if  t  is  a  pair  then  a  otherwise  b  \msim{}  b))))


By

---

Latex:
(Auto
  THEN  InstLemma  `has-value-implies-dec-ispair`  [\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto
  THEN  CanonicalTestCases
  THEN  Auto
  THEN  HypSubst  (-1)  (-4)
  THEN  Reduce  (-4)
  THEN  FLemma  `not\_zero\_sqequal\_one`  [-4]
  THEN  Trivial)

---

Home Index