---

Step * of Lemma callbyvalue-exception-type

∀[T:Type]. ∀[x:T]. ∀[B:Top].  eval z = x in B[z] ~ 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)
⊢ eval z = a in
  B[z] ~ a

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[B:Top].    eval  z  =  x  in  B[z]  \msim{}  x  supposing  exception-type(T)


By

---

Latex:
(Auto  THEN  PointwiseFunctionality  2)

---

Home Index