---

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