---

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

.....subterm..... T:t
2:n
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'
⊢ a1 = b' ∈ A
BY
{ (BackThruHyp' 2⋅ THEN Auto) }

1
1. A : Type
2. ∀a:A. ∀b:Base.  (is-above(A;a;b) ⇒ (a = b ∈ 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'
⊢ is-above(A;a1;b')

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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'
\mvdash{}  a1  =  b'


By

---

Latex:
(BackThruHyp'  2\mcdot{}  THEN  Auto)

---

Home Index