---

Step * 1 of Lemma is-above-inr


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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index