---

Step * of Lemma bar_fwd_fim_wf

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


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


By

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



Home Index