---

Step * of Lemma rec-comb_wf2

∀[Info:Type]. ∀[n,m:ℕ]. ∀[A:{m..n-} ⟶ Type]. ∀[X:i:{m..n-} ⟶ EClass(A i)]. ∀[T:Type]. ∀[f:Id
                                                                                            ⟶ (i:{m..n-} ⟶ bag(A i))
                                                                                            ⟶ bag(T)
                                                                                            ⟶ bag(T)].
∀[init:Id ⟶ bag(T)].
  (rec-comb(X;f;init) ∈ EClass(T))
BY
{ (BasicUniformUnivCD Auto THEN All (Unfold `eclass`) THEN Unhide) }

1
1. Info : Type
2. n : ℕ
3. m : ℕ
4. A : {m..n-} ⟶ Type
5. X : i:{m..n-} ⟶ es:EO+(Info) ⟶ e:E ⟶ bag(A i)
6. T : Type
7. f : Id ⟶ (i:{m..n-} ⟶ bag(A i)) ⟶ bag(T) ⟶ bag(T)
8. init : Id ⟶ bag(T)
⊢ rec-comb(X;f;init) ∈ es:EO+(Info) ⟶ e:E ⟶ bag(T)

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[n,m:\mBbbN{}].  \mforall{}[A:\{m..n\msupminus{}\}  {}\mrightarrow{}  Type].  \mforall{}[X:i:\{m..n\msupminus{}\}  {}\mrightarrow{}  EClass(A  i)].  \mforall{}[T:Type].
\mforall{}[f:Id  {}\mrightarrow{}  (i:\{m..n\msupminus{}\}  {}\mrightarrow{}  bag(A  i))  {}\mrightarrow{}  bag(T)  {}\mrightarrow{}  bag(T)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(T)].
    (rec-comb(X;f;init)  \mmember{}  EClass(T))


By

---

Latex:
(BasicUniformUnivCD  Auto  THEN  All  (Unfold  `eclass`)  THEN  Unhide)

---

Home Index