---

Step * of Lemma interleaved_family_occurence_wf

∀[T,I:Type]. ∀[L:I ⟶ (T List)]. ∀[L2:T List]. ∀[f:i:I ⟶ ℕ||L i|| ⟶ ℕ||L2||].
  (interleaved_family_occurence(T;I;L;L2;f) ∈ ℙ)
BY
{ (Unfold `interleaved_family_occurence` 0 THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T,I:Type].  \mforall{}[L:I  {}\mrightarrow{}  (T  List)].  \mforall{}[L2:T  List].  \mforall{}[f:i:I  {}\mrightarrow{}  \mBbbN{}||L  i||  {}\mrightarrow{}  \mBbbN{}||L2||].
    (interleaved\_family\_occurence(T;I;L;L2;f)  \mmember{}  \mBbbP{})


By

---

Latex:
(Unfold  `interleaved\_family\_occurence`  0  THEN  Auto')

---

Home Index