---

Step * 1 1 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)>
⊢ is-above(A;a;fst(z))
BY
{ ((With ⌜fst(y)⌝ (D 0)⋅ THENA Auto)
   THEN Try ((MemCD THEN Try (BLemma `equal-wf-base-T`) THEN Auto))
   THEN D 0
   THEN Try (Trivial)) }

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)>
⊢ fst(y) ≤ fst(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)>
\mvdash{}  is-above(A;a;fst(z))


By

---

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

---

Home Index