---

Step * of Lemma norm-list_wf_sq

∀[T:Type]. (∀[N:sq-id-fun(T)]. (norm-list(N) ∈ sq-id-fun(T List))) supposing (value-type(T) and (T ⊆r Base))
BY
{ (Auto
   THEN (InstLemma `subtype_base_sq` [⌜T List⌝]⋅
         THENA (Auto THEN (D 0 THEN Auto) THEN ListInd (-1)⋅ THEN Auto THEN DoSubsume ⋅ THEN Auto)
         )
   THEN (InstLemma `subtype_base_sq` [⌜T⌝]⋅ THENA Auto)
   THEN Unfold `sq-id-fun` 0
   THEN ExtWith [`L'] [⌜Top ⟶ Top⌝]⋅
   THEN Auto
   THEN Try (ProveWfLemma)) }

1
1. T : Type
2. T ⊆r Base
3. value-type(T)
4. N : sq-id-fun(T)
5. SQType(T List)
6. SQType(T)
7. L : T List
⊢ norm-list(N) L ∈ {y:T List| L ~ y} 

---

Latex:

---

Latex:
\mforall{}[T:Type]
    (\mforall{}[N:sq-id-fun(T)].  (norm-list(N)  \mmember{}  sq-id-fun(T  List)))  supposing  (value-type(T)  and  (T  \msubseteq{}r  Base))


By

---

Latex:
(Auto
  THEN  (InstLemma  `subtype\_base\_sq`  [\mkleeneopen{}T  List\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  (D  0  THEN  Auto)  THEN  ListInd  (-1)\mcdot{}  THEN  Auto  THEN  DoSubsume  \mcdot{}  THEN  Auto)
              )
  THEN  (InstLemma  `subtype\_base\_sq`  [\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `sq-id-fun`  0
  THEN  ExtWith  [`L']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (ProveWfLemma))

---

Home Index