---

Step * 1 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. z ~ <fst(z), snd(z)>
12. z ~ <fst(z), snd(z)>
13. is-above(A;a;fst(z))
⊢ is-above(B[a];b;snd(z))
BY
{ (With ⌜snd(y)⌝ (D 0)⋅
   THEN Try ((MemCD THEN Try (BLemma `equal-wf-base-T`) THEN Auto))
   THEN D 0
   THEN Try (Complete (Auto)))⋅ }

1
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. z ~ <fst(z), snd(z)>
12. z ~ <fst(z), snd(z)>
13. is-above(A;a;fst(z))
⊢ snd(y) ≤ snd(z)

---

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.  z  \msim{}  <fst(z),  snd(z)>
12.  z  \msim{}  <fst(z),  snd(z)>
13.  is-above(A;a;fst(z))
\mvdash{}  is-above(B[a];b;snd(z))


By

---

Latex:
(With  \mkleeneopen{}snd(y)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Try  ((MemCD  THEN  Try  (BLemma  `equal-wf-base-T`)  THEN  Auto))
  THEN  D  0
  THEN  Try  (Complete  (Auto)))\mcdot{}

---

Home Index