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` 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