---

Step * of Lemma bar_fwd_fim_classical_wf

R: List  . (bar_fwd_fim_classical(R)  )
BY
{ ((Auto THEN Unfold `bar_fwd_fim_classical` 0) THEN Auto) }


\mforall{}R:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.  (bar\_fwd\_fim\_classical(R)  \mmember{}  \mBbbP{})


By

((Auto  THEN  Unfold  `bar\_fwd\_fim\_classical`  0)  THEN  Auto)



Home Index