---

Step * 1 of Lemma is-above-inl


1. [A] : Type
2. [B] : Type
3. [a] : A
4. z : Base
5. y : Base
6. y = (inl a) ∈ (A + B)
7. y ≤ z
8. ∃c:Base. (y ~ inl c)
⊢ (z ~ inl outl(z)) ∧ is-above(A;a;outl(z))
BY
{ (ExRepD
   THEN (Assert ((inl c) = (inl a) ∈ (A + B)) ∧ (inl c ≤ z) BY
               (RevHypSubst' (-1) 0 THEN Auto))
   THEN D -1
   THEN All Reduce)⋅ }

1
1. [A] : Type
2. [B] : Type
3. [a] : A
4. z : Base
5. y : Base
6. y = (inl a) ∈ (A + B)
7. y ≤ z
8. c : Base
9. y ~ inl c
10. (inl c) = (inl a) ∈ (A + B)
11. inl c ≤ z
⊢ (z ~ inl outl(z)) ∧ is-above(A;a;outl(z))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [a]  :  A
4.  z  :  Base
5.  y  :  Base
6.  y  =  (inl  a)
7.  y  \mleq{}  z
8.  \mexists{}c:Base.  (y  \msim{}  inl  c)
\mvdash{}  (z  \msim{}  inl  outl(z))  \mwedge{}  is-above(A;a;outl(z))


By

---

Latex:
(ExRepD
  THEN  (Assert  ((inl  c)  =  (inl  a))  \mwedge{}  (inl  c  \mleq{}  z)  BY
                          (RevHypSubst'  (-1)  0  THEN  Auto))
  THEN  D  -1
  THEN  All  Reduce)\mcdot{}

---

Home Index