---

Step * of Lemma ext-eq-implies-biject

∀[T,S:Type].  (T ≡ S ⇒ Bij(S;T;λx.x))
BY
{ Auto }

1
1. [T] : Type
2. [S] : Type
3. T ≡ S
⊢ Bij(S;T;λx.x)

---

Latex:

---

Latex:
\mforall{}[T,S:Type].    (T  \mequiv{}  S  {}\mRightarrow{}  Bij(S;T;\mlambda{}x.x))


By

---

Latex:
Auto

---

Home Index