---

Step * 1 1 1 2 of Lemma polymorphic-constant-base


1. T : Type
2. mono(T)
3. value-type(T)
4. f : Base
5. f1 : Base
6. f = f1 ∈ (Base ⟶ T)
7. x : Base
8. (f x) = (f ⊥) ∈ T
⊢ (f x) = (f1 ⊥) ∈ T
BY
{ Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  mono(T)
3.  value-type(T)
4.  f  :  Base
5.  f1  :  Base
6.  f  =  f1
7.  x  :  Base
8.  (f  x)  =  (f  \mbot{})
\mvdash{}  (f  x)  =  (f1  \mbot{})


By

---

Latex:
Auto

---

Home Index