---

Step * 1 of Lemma function-mono


1. A : Type
2. B : A ⟶ Type
3. A ⊆r Base
4. ∀a:A. mono(B[a])
5. ∃a:A. value-type(B[a])
6. f : a:A ⟶ B[a]
7. g : Base
8. h : Base
9. h = f ∈ (a:A ⟶ B[a])
10. h ≤ g
⊢ f = g ∈ (a:A ⟶ B[a])
BY
{ ((FunExt THENA Auto) THEN (InstHyp [⌜a⌝] 4⋅ THENA Auto)) }

1
1. A : Type
2. B : A ⟶ Type
3. A ⊆r Base
4. ∀a:A. mono(B[a])
5. ∃a:A. value-type(B[a])
6. f : a:A ⟶ B[a]
7. g : Base
8. h : Base
9. h = f ∈ (a:A ⟶ B[a])
10. h ≤ g
11. a : A
12. mono(B[a])
⊢ (f a) = (g a) ∈ B[a]

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  A  \msubseteq{}r  Base
4.  \mforall{}a:A.  mono(B[a])
5.  \mexists{}a:A.  value-type(B[a])
6.  f  :  a:A  {}\mrightarrow{}  B[a]
7.  g  :  Base
8.  h  :  Base
9.  h  =  f
10.  h  \mleq{}  g
\mvdash{}  f  =  g


By

---

Latex:
((FunExt  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  4\mcdot{}  THENA  Auto))

---

Home Index