Step
*
of Lemma
equipollent-subtype
∀[T,A:Type].
(∀[a,b:ℕ]. (a ≤ b) supposing (T ~ ℕb and A ~ ℕa)) supposing
((∀a1,a2:A. ((a1 = a2 ∈ T)
⇒ (a1 = a2 ∈ A))) and
(A ⊆r T))
BY
{ Auto }
1
1. T : Type
2. A : Type
3. A ⊆r T
4. ∀a1,a2:A. ((a1 = a2 ∈ T)
⇒ (a1 = a2 ∈ A))
5. a : ℕ
6. b : ℕ
7. A ~ ℕa
8. T ~ ℕb
⊢ a ≤ b
Latex:
Latex:
\mforall{}[T,A:Type].
(\mforall{}[a,b:\mBbbN{}]. (a \mleq{} b) supposing (T \msim{} \mBbbN{}b and A \msim{} \mBbbN{}a)) supposing
((\mforall{}a1,a2:A. ((a1 = a2) {}\mRightarrow{} (a1 = a2))) and
(A \msubseteq{}r T))
By
Latex:
Auto
Home
Index