---

Step * of Lemma polymorphic-constant-base

∀[T:Type]. ∀f:Base ⟶ T. ∃t:T. ∀x:Base. ((f x) = t ∈ T) supposing mono(T) ∧ value-type(T)
BY
{ (Auto THEN (With ⌜f ⊥⌝ (D 0)⋅ THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}f:Base  {}\mrightarrow{}  T.  \mexists{}t:T.  \mforall{}x:Base.  ((f  x)  =  t)  supposing  mono(T)  \mwedge{}  value-type(T)


By

---

Latex:
(Auto  THEN  (With  \mkleeneopen{}f  \mbot{}\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto))

---

Home Index