---

Step * of Lemma subtype_rel_tuple-type

∀[As,Bs:Type List].  tuple-type(As) ⊆r tuple-type(Bs) supposing (||As|| = ||Bs|| ∈ ℤ) ∧ (∀i:ℕ||As||. (As[i] ⊆r Bs[i]))
BY
{ (RepeatFor 2 (InductionOnList)
   THEN Auto'
   THEN Reduce 0
   THEN (InstHyp [⌜0⌝] (-1)⋅ THENA Auto')
   THEN Reduce (-1)
   THEN RepeatFor 2 (AutoSplit)
   THEN Try ((DVar `v' THEN DVar `v1' THEN All Reduce THEN Complete (Auto'))⋅)) }

1
1. u : Type
2. v : Type List
3. ¬(v = [] ∈ (Type List))
4. ∀[Bs:Type List]. tuple-type(v) ⊆r tuple-type(Bs) supposing (||v|| = ||Bs|| ∈ ℤ) ∧ (∀i:ℕ||v||. (v[i] ⊆r Bs[i]))
5. u1 : Type
6. v1 : Type List
7. ¬(v1 = [] ∈ (Type List))
8. tuple-type([u / v]) ⊆r tuple-type(v1) supposing (||[u / v]|| = ||v1|| ∈ ℤ) ∧ (∀i:ℕ||[u / v]||. ([u / v][i] ⊆r v1[i]))
9. ||[u / v]|| = ||[u1 / v1]|| ∈ ℤ
10. ∀i:ℕ||[u / v]||. ([u / v][i] ⊆r [u1 / v1][i])
11. u ⊆r u1
⊢ (u × tuple-type(v)) ⊆r (u1 × tuple-type(v1))

---

Latex:

---

Latex:
\mforall{}[As,Bs:Type  List].
    tuple-type(As)  \msubseteq{}r  tuple-type(Bs)  supposing  (||As||  =  ||Bs||)  \mwedge{}  (\mforall{}i:\mBbbN{}||As||.  (As[i]  \msubseteq{}r  Bs[i]))


By

---

Latex:
(RepeatFor  2  (InductionOnList)
  THEN  Auto'
  THEN  Reduce  0
  THEN  (InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto')
  THEN  Reduce  (-1)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  Try  ((DVar  `v'  THEN  DVar  `v1'  THEN  All  Reduce  THEN  Complete  (Auto'))\mcdot{}))

---

Home Index