---

Step * of Lemma spread-exception-type

∀[T:Type]. ∀[x:T]. ∀[B:Top].  let u,v = x in B[u;v] ~ x supposing exception-type(T)
BY
{ (Auto THEN PointwiseFunctionality 2) }

1
1. T : Type
2. [a] : Base
3. [b] : Base
4. [c] : a = b ∈ T
5. B : Top
6. exception-type(T)
⊢ let u,v = a 
  in B[u;v] ~ a

2
1. T : Type
2. a : Base
3. b : Base
4. c : a = b ∈ T
5. B : Top
6. exception-type(T)
⊢ (let u,v = a in B[u;v] ~ a) = (let u,v = b in B[u;v] ~ b) ∈ Type

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[B:Top].    let  u,v  =  x  in  B[u;v]  \msim{}  x  supposing  exception-type(T)


By

---

Latex:
(Auto  THEN  PointwiseFunctionality  2)

---

Home Index