---

Step * of Lemma awf-system-subtype

∀[I,A:Type].  (awf-system{i:l}(I;A) ⊆r ((I ⟶ awf(A)) ⟶ I ⟶ awf(A)))
BY
{ xxx(Auto
      THEN (InstLemma `corec-ext` [⌜λ2T.A + (T List)⌝]⋅ THENA Auto)
      THEN Fold `awf` (-1)
      THEN Assert ⌜(A + (awf(A) List)) ⊆r awf(A)⌝⋅
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[I,A:Type].    (awf-system\{i:l\}(I;A)  \msubseteq{}r  ((I  {}\mrightarrow{}  awf(A))  {}\mrightarrow{}  I  {}\mrightarrow{}  awf(A)))


By

---

Latex:
xxx(Auto
        THEN  (InstLemma  `corec-ext`  [\mkleeneopen{}\mlambda{}\msubtwo{}T.A  +  (T  List)\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  Fold  `awf`  (-1)
        THEN  Assert  \mkleeneopen{}(A  +  (awf(A)  List))  \msubseteq{}r  awf(A)\mkleeneclose{}\mcdot{}
        THEN  Auto)xxx

---

Home Index