---

Step * of Lemma is-above-inr

∀[A,B:Type]. ∀[a:B].  ∀z:Base. (is-above(A + B;inr a ;z) ⇒ (∃c:Base. ((z ~ inr c ) ∧ is-above(B;a;c))))
BY
{ (Auto
   THEN (InstConcl [⌜outr(z)⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (D (-1))
   THEN (Assert ∃c:Base. (y ~ inr c ) BY
               ((InstConcl [⌜outr(y)⌝ ]⋅ THENA Auto)
                THEN (Assert ⌜↑isr(y)⌝⋅ BY
                            (HypSubst' (-2) 0 THEN Auto))
                THEN MoveToConcl (-1)
                THEN (GenConcl ⌜y = u ∈ (A + B)⌝⋅ THENA Auto)
                THEN D -2
                THEN Reduce 0
                THEN Auto))⋅) }

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. (y ~ inr c )
⊢ (z ~ inr outr(z) ) ∧ is-above(B;a;outr(z))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[a:B].
    \mforall{}z:Base.  (is-above(A  +  B;inr  a  ;z)  {}\mRightarrow{}  (\mexists{}c:Base.  ((z  \msim{}  inr  c  )  \mwedge{}  is-above(B;a;c))))


By

---

Latex:
(Auto
  THEN  (InstConcl  [\mkleeneopen{}outr(z)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  (-1))
  THEN  (Assert  \mexists{}c:Base.  (y  \msim{}  inr  c  )  BY
                          ((InstConcl  [\mkleeneopen{}outr(y)\mkleeneclose{}  ]\mcdot{}  THENA  Auto)
                            THEN  (Assert  \mkleeneopen{}\muparrow{}isr(y)\mkleeneclose{}\mcdot{}  BY
                                                    (HypSubst'  (-2)  0  THEN  Auto))
                            THEN  MoveToConcl  (-1)
                            THEN  (GenConcl  \mkleeneopen{}y  =  u\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  Auto))\mcdot{})

---

Home Index