---

Step * 1 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
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))
BY
{ ((FLemma `has-value-monotonic` [-1] THENA (Reduce 0 THEN Auto))
   THEN ((FLemma `has-value-implies-dec-isinl-2` [-1]⋅ THENM D -1) THENA 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
9. y ~ inl c
10. (inl c) = (inl a) ∈ (A + B)
11. inl c ≤ z
12. (z)↓
13. z ~ inl outl(z)
⊢ (z ~ inl outl(z)) ∧ is-above(A;a;outl(z))

2
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
12. (z)↓
13. ∀a,b:Base.  (if z is inl then a else b ~ b)
⊢ (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.  c  :  Base
9.  y  \msim{}  inl  c
10.  (inl  c)  =  (inl  a)
11.  inl  c  \mleq{}  z
\mvdash{}  (z  \msim{}  inl  outl(z))  \mwedge{}  is-above(A;a;outl(z))


By

---

Latex:
((FLemma  `has-value-monotonic`  [-1]  THENA  (Reduce  0  THEN  Auto))
  THEN  ((FLemma  `has-value-implies-dec-isinl-2`  [-1]\mcdot{}  THENM  D  -1)  THENA  Auto)
  )\mcdot{}

---

Home Index