---

Step * 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)>
⊢ (z ~ <fst(z), snd(z)>) ∧ is-above(A;a;fst(z)) ∧ is-above(B[a];b;snd(z))
BY
{ TACTIC: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)>
⊢ is-above(A;a;fst(z))

2
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))

---

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)>
\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:Auto

---

Home Index