---

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

∀t:Base. ((t)↓ ⇒ ((t ~ inl outl(t)) ∨ (∀a,b:Base.  (if t is inl then a else b ~ b))))
BY
{ (Auto
   THEN InstLemma `has-value-implies-dec-isinl` [⌜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{}  inl  outl(t))  \mvee{}  (\mforall{}a,b:Base.    (if  t  is  inl  then  a  else  b  \msim{}  b))))


By

---

Latex:
(Auto
  THEN  InstLemma  `has-value-implies-dec-isinl`  [\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