---

Step * of Lemma apply-exception-type

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  PointwiseFunctionality  2)

---

Home Index