---

Step * 2 of Lemma t-sqle-apply-dependent


1. A : Type
2. mono(A)
3. B : A ⟶ Type
4. a1 : A
5. a2 : A
6. f1 : a:A ⟶ B[a]
7. f2 : a:A ⟶ B[a]
8. a3 : Base
9. a3 = f1 ∈ (a:A ⟶ B[a])
10. b1 : Base
11. b1 = f2 ∈ (a:A ⟶ B[a])
12. a3 ≤ b1
13. a' : Base
14. a' = a1 ∈ A
15. b' : Base
16. b' = a2 ∈ A
17. a' ≤ b'
18. B[a1] = B[b'] ∈ Type
⊢ ∃a':{x:Base| x = (f1 a1) ∈ B[a1]} . ∃b':{x:Base| x = (f2 a2) ∈ B[a1]} . (a' ≤ b')
BY
{ (InstConcl [⌜a3 a'⌝;⌜b1 b'⌝]⋅
   THEN Try ((SqLeCD THEN Hypothesis))
   THEN Try ((MemTypeCD THEN Try (BLemma `equal-wf-base-T`) THEN Auto))
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  mono(A)
3.  B  :  A  {}\mrightarrow{}  Type
4.  a1  :  A
5.  a2  :  A
6.  f1  :  a:A  {}\mrightarrow{}  B[a]
7.  f2  :  a:A  {}\mrightarrow{}  B[a]
8.  a3  :  Base
9.  a3  =  f1
10.  b1  :  Base
11.  b1  =  f2
12.  a3  \mleq{}  b1
13.  a'  :  Base
14.  a'  =  a1
15.  b'  :  Base
16.  b'  =  a2
17.  a'  \mleq{}  b'
18.  B[a1]  =  B[b']
\mvdash{}  \mexists{}a':\{x:Base|  x  =  (f1  a1)\}  .  \mexists{}b':\{x:Base|  x  =  (f2  a2)\}  .  (a'  \mleq{}  b')


By

---

Latex:
(InstConcl  [\mkleeneopen{}a3  a'\mkleeneclose{};\mkleeneopen{}b1  b'\mkleeneclose{}]\mcdot{}
  THEN  Try  ((SqLeCD  THEN  Hypothesis))
  THEN  Try  ((MemTypeCD  THEN  Try  (BLemma  `equal-wf-base-T`)  THEN  Auto))
  THEN  Auto)\mcdot{}

---

Home Index