---

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


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
BY
{ xxxAssert ⌜(f x) = (f ⊥) ∈ T⌝⋅xxx }

1
.....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

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

---

Latex:

---

Latex:

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)  =  (f1  \mbot{})


By

---

Latex:
xxxAssert  \mkleeneopen{}(f  x)  =  (f  \mbot{})\mkleeneclose{}\mcdot{}xxx

---

Home Index