---

Step * of Lemma type-incr-chain-subtype

∀[X:type-incr-chain{i:l}()]. ∀[n,m:ℕ].  (X n) ⊆r (X m) supposing n ≤ m
BY
{ (Auto
   THEN (Assert ∀k:ℕ. ((X n) ⊆r (X (n + k))) BY
               (InductionOnNat
                THEN Auto
                THEN Subst' n + k ~ (n + (k - 1)) + 1 0
                THEN Auto
                THEN RWO "-1" 0
                THEN Auto
                THEN D 1
                THEN Unhide
                THEN Auto))
   ) }

1
1. X : type-incr-chain{i:l}()
2. n : ℕ
3. m : ℕ
4. n ≤ m
5. ∀k:ℕ. ((X n) ⊆r (X (n + k)))
⊢ (X n) ⊆r (X m)

---

Latex:

---

Latex:
\mforall{}[X:type-incr-chain\{i:l\}()].  \mforall{}[n,m:\mBbbN{}].    (X  n)  \msubseteq{}r  (X  m)  supposing  n  \mleq{}  m


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}k:\mBbbN{}.  ((X  n)  \msubseteq{}r  (X  (n  +  k)))  BY
                          (InductionOnNat
                            THEN  Auto
                            THEN  Subst'  n  +  k  \msim{}  (n  +  (k  -  1))  +  1  0
                            THEN  Auto
                            THEN  RWO  "-1"  0
                            THEN  Auto
                            THEN  D  1
                            THEN  Unhide
                            THEN  Auto))
  )

---

Home Index