---

Step * of Lemma decide-exception-type

∀[T:Type]. ∀[x:T]. ∀[A,B:Top].  case x of inl(u) => A[u] | inr(v) => B[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. A : Top
6. B : Top
7. exception-type(T)
⊢ case a of inl(u) => A[u] | inr(v) => B[v] ~ a

2
1. T : Type
2. a : Base
3. b : Base
4. c : a = b ∈ T
5. A : Top
6. B : Top
7. exception-type(T)
⊢ (case a of inl(u) => A[u] | inr(v) => B[v] ~ a) = (case b of inl(u) => A[u] | inr(v) => B[v] ~ b) ∈ Type

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[A,B:Top].
    case  x  of  inl(u)  =>  A[u]  |  inr(v)  =>  B[v]  \msim{}  x  supposing  exception-type(T)


By

---

Latex:
(Auto  THEN  PointwiseFunctionality  2)

---

Home Index