---

Step * of Lemma unique-awf

∀[A,I:Type].
  ∀G:awf-system{i:l}(I;A)
    (∃s:I ⟶ awf(A) [((∀i:I. ((s i) = (G s i) ∈ awf(A)))
                    ∧ (∀s':I ⟶ awf(A). ((∀i:I. ((s' i) = (G s' i) ∈ awf(A))) ⇒ (s' = s ∈ (I ⟶ awf(A))))))])
BY
{ TACTIC:(Unfold `awf-system` 0
          THEN Auto⋅
          THEN ((InstLemma `unique-corec-solution` [⌜λ2T.A + (T List)⌝;⌜I⌝;⌜G⌝]⋅ THENM (Fold `awf` (-1) THEN Auto))
                THENA Auto
                )) }

1
1. [A] : Type
2. [I] : Type
3. G : ⋂T:{T:Type| ((A + (T List)) ⊆r T) ∧ (awf(A) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ (A + (T List))) ⋂ Top ⟶ I ⟶ Top@i'
4. ∃!s:I ⟶ awf(A). (s = (G s) ∈ (I ⟶ awf(A)))
⊢ ∃s:I ⟶ awf(A) [((∀i:I. ((s i) = (G s i) ∈ awf(A)))
                 ∧ (∀s':I ⟶ awf(A). ((∀i:I. ((s' i) = (G s' i) ∈ awf(A))) ⇒ (s' = s ∈ (I ⟶ awf(A))))))]

---

Latex:

---

Latex:
\mforall{}[A,I:Type].
    \mforall{}G:awf-system\{i:l\}(I;A)
        (\mexists{}s:I  {}\mrightarrow{}  awf(A)  [((\mforall{}i:I.  ((s  i)  =  (G  s  i)))
                                        \mwedge{}  (\mforall{}s':I  {}\mrightarrow{}  awf(A).  ((\mforall{}i:I.  ((s'  i)  =  (G  s'  i)))  {}\mRightarrow{}  (s'  =  s))))])


By

---

Latex:
TACTIC:(Unfold  `awf-system`  0
                THEN  Auto\mcdot{}
                THEN  ((InstLemma  `unique-corec-solution`  [\mkleeneopen{}\mlambda{}\msubtwo{}T.A  +  (T  List)\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{}]\mcdot{}
                            THENM  (Fold  `awf`  (-1)  THEN  Auto)
                            )
                            THENA  Auto
                            ))

---

Home Index