---

Step * 1 of Lemma polymorphic-constant-base


1. [T] : Type
2. mono(T)
3. value-type(T)
4. f : Base ⟶ T
⊢ ∀x:Base. ((f x) = (f ⊥) ∈ T)
BY
{ xxx(D 0 THENA Auto)xxx }

1
1. T : Type
2. mono(T)
3. value-type(T)
4. f : Base ⟶ T
5. x : Base
⊢ (f x) = (f ⊥) ∈ T

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  mono(T)
3.  value-type(T)
4.  f  :  Base  {}\mrightarrow{}  T
\mvdash{}  \mforall{}x:Base.  ((f  x)  =  (f  \mbot{}))


By

---

Latex:
xxx(D  0  THENA  Auto)xxx

---

Home Index