---

Step * of Lemma polymorphic-constant

∀[T:Type]. ∀f:⋂A:Type. (A ⟶ T). ∃t:T. ∀A:Type. ∀x:A.  ((f x) = t ∈ T) supposing mono(T) ∧ value-type(T)
BY
{ xxx(Auto THEN (InstLemma `polymorphic-constant-base` [⌜T⌝;⌜f⌝]⋅ THEN Auto) THEN ParallelLast THEN Auto)xxx }

1
1. T : Type
2. mono(T)
3. value-type(T)
4. f : ⋂A:Type. (A ⟶ T)
5. t : T
6. ∀x:Base. ((f x) = t ∈ T)
7. A : Type
8. x : A
⊢ (f x) = t ∈ T

---

Latex:

---

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


By

---

Latex:
xxx(Auto
        THEN  (InstLemma  `polymorphic-constant-base`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto)
        THEN  ParallelLast
        THEN  Auto)xxx

---

Home Index