---

Step * of Lemma ispair-pair

∀[t,x,y:Base].  t ∈ Top × Top supposing if t is a pair then inl x otherwise inr y  ~ inl x
BY
{ (Auto
   THEN (Assert ⌜(if t is a pair then inl x otherwise inr y )↓⌝⋅ THENA (HypSubst (-1) 0 THEN Reduce 0 THEN Auto))
   THEN HasValueD  (-1)
   THEN MoveToConcl (-3)
   THEN CanonicalTestCases
   THEN Try (Complete (Auto))
   THEN (D 0 THENA Auto)) }

1
1. t : Base
2. x : Base
3. y : Base
4. (if t is a pair then inl x otherwise inr y )↓
5. (t)↓
6. ∀[u,v:Top].  (if t is a pair then u otherwise v ~ v)
7. inr y  ~ inl x@i
⊢ t ∈ Top × Top

---

Latex:

---

Latex:
\mforall{}[t,x,y:Base].    t  \mmember{}  Top  \mtimes{}  Top  supposing  if  t  is  a  pair  then  inl  x  otherwise  inr  y    \msim{}  inl  x


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}(if  t  is  a  pair  then  inl  x  otherwise  inr  y  )\mdownarrow{}\mkleeneclose{}\mcdot{}
              THENA  (HypSubst  (-1)  0  THEN  Reduce  0  THEN  Auto)
              )
  THEN  HasValueD    (-1)
  THEN  MoveToConcl  (-3)
  THEN  CanonicalTestCases
  THEN  Try  (Complete  (Auto))
  THEN  (D  0  THENA  Auto))

---

Home Index