---

Step * 1 1 1 of Lemma unique-awf


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. G ∈ Top ⟶ I ⟶ Top
5. G ∈ ⋂T:{T:Type| ((A + (T List)) ⊆r T) ∧ (awf(A) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ (A + (T List)))
⊢ G ∈ (I ⟶ awf(A)) ⟶ I ⟶ awf(A)
BY
{ ((InstLemma `corec-ext` [⌜λ2T.A + (T List)⌝]⋅ THENM (Fold `awf` (-1) THEN D -1)) 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. G ∈ Top ⟶ I ⟶ Top
5. G ∈ ⋂T:{T:Type| ((A + (T List)) ⊆r T) ∧ (awf(A) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ (A + (T List)))
6. awf(A) ⊆r (A + (awf(A) List))
7. (A + (awf(A) List)) ⊆r awf(A)
⊢ G ∈ (I ⟶ awf(A)) ⟶ I ⟶ awf(A)

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [I]  :  Type
3.  G  :  \mcap{}T:\{T:Type|  ((A  +  (T  List))  \msubseteq{}r  T)  \mwedge{}  (awf(A)  \msubseteq{}r  T)\}  .  ((I  {}\mrightarrow{}  T)  {}\mrightarrow{}  I  {}\mrightarrow{}  (A  +  (T  List)))  \mcap{}  Top
{}\mrightarrow{}  I
{}\mrightarrow{}  Top@i'
4.  G  \mmember{}  Top  {}\mrightarrow{}  I  {}\mrightarrow{}  Top
5.  G  \mmember{}  \mcap{}T:\{T:Type|  ((A  +  (T  List))  \msubseteq{}r  T)  \mwedge{}  (awf(A)  \msubseteq{}r  T)\}  .  ((I  {}\mrightarrow{}  T)  {}\mrightarrow{}  I  {}\mrightarrow{}  (A  +  (T  List)))
\mvdash{}  G  \mmember{}  (I  {}\mrightarrow{}  awf(A))  {}\mrightarrow{}  I  {}\mrightarrow{}  awf(A)


By

---

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

---

Home Index