---

Step * 2 of Lemma is-above-pair


1. [A] : Type
2. [B] : A ⟶ Type
3. [a] : A
4. [b] : B[a]
5. z : Base
6. y : Base
7. (fst(y)) = a ∈ A
8. (snd(y)) = b ∈ B[fst(y)]
9. <fst(y), snd(y)> ≤ z
10. (z)↓
11. ∀a,b:Base.  (if z is a pair then a otherwise b ~ b)
⊢ (z ~ <fst(z), snd(z)>) ∧ is-above(A;a;fst(z)) ∧ is-above(B[a];b;snd(z))
BY
{ TACTIC:(Assert ⌜False⌝⋅
          THEN Auto
          THEN (Assert ⌜ispair(<fst(y), snd(y)>) ≤ ispair(z)⌝⋅
                THEN Auto
                THEN Reduce (-1)
                THEN (RWO "-2" (-1) THENA Auto)
                THEN InstLemma `not-btrue-sqle-bfalse` []
                THEN Auto)⋅⋅) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  [a]  :  A
4.  [b]  :  B[a]
5.  z  :  Base
6.  y  :  Base
7.  (fst(y))  =  a
8.  (snd(y))  =  b
9.  <fst(y),  snd(y)>  \mleq{}  z
10.  (z)\mdownarrow{}
11.  \mforall{}a,b:Base.    (if  z  is  a  pair  then  a  otherwise  b  \msim{}  b)
\mvdash{}  (z  \msim{}  <fst(z),  snd(z)>)  \mwedge{}  is-above(A;a;fst(z))  \mwedge{}  is-above(B[a];b;snd(z))


By

---

Latex:
TACTIC:(Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
                THEN  Auto
                THEN  (Assert  \mkleeneopen{}ispair(<fst(y),  snd(y)>)  \mleq{}  ispair(z)\mkleeneclose{}\mcdot{}
                            THEN  Auto
                            THEN  Reduce  (-1)
                            THEN  (RWO  "-2"  (-1)  THENA  Auto)
                            THEN  InstLemma  `not-btrue-sqle-bfalse`  []
                            THEN  Auto)\mcdot{}\mcdot{})

---

Home Index