---

Step * of Lemma is-above-inl

∀[A,B:Type]. ∀[a:A].  ∀z:Base. (is-above(A + B;inl a;z) ⇒ (∃c:Base. ((z ~ inl c) ∧ is-above(A;a;c))))
BY
{ (Auto
   THEN (InstConcl [⌜outl(z)⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (D (-1))
   THEN (Assert ∃c:Base. (y ~ inl c) BY
               ((InstConcl [⌜outl(y)⌝ ]⋅ THENA Auto)
                THEN (Assert ⌜↑isl(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] : 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))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstConcl  [\mkleeneopen{}outl(z)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  (-1))
  THEN  (Assert  \mexists{}c:Base.  (y  \msim{}  inl  c)  BY
                          ((InstConcl  [\mkleeneopen{}outl(y)\mkleeneclose{}  ]\mcdot{}  THENA  Auto)
                            THEN  (Assert  \mkleeneopen{}\muparrow{}isl(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