---

Step * 1 1 of Lemma polymorphic-constant-base


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(PointwiseFunctionalityForEquality  4  THENA  Auto)xxx

---

Home Index