---

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

.....assertion..... 
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) = (f ⊥) ∈ T
BY
{ (Symmetry THEN (With ⌜f ⊥⌝ (D 2)⋅ THENA Auto)) }

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

2
1. T : Type
2. value-type(T)
3. f : Base
4. f1 : Base
5. f = f1 ∈ (Base ⟶ T)
6. x : Base
7. ∀b:Base. (is-above(T;f ⊥;b) ⇒ ((f ⊥) = b ∈ T))
⊢ (f ⊥) = (f x) ∈ T

---

Latex:

---

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


By

---

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

---

Home Index