---

Step * of Lemma ispair-implies

∀[t:Base]. (t ~ <fst(t), snd(t)>) supposing ((↑ispair(t)) and (t)↓)
BY
{ ((UnivCD THENA Auto)
   THEN Try ((BLemma `ispair-bool-if-has-value` THEN Auto))
   THEN MoveToConcl (-1)
   THEN CanonicalTestCases
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[t:Base].  (t  \msim{}  <fst(t),  snd(t)>)  supposing  ((\muparrow{}ispair(t))  and  (t)\mdownarrow{})


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Try  ((BLemma  `ispair-bool-if-has-value`  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  CanonicalTestCases
  THEN  Reduce  0
  THEN  Auto)

---

Home Index