Step * of Lemma bar_bwd_fim_classical_wf

R,A: List  .  (bar_bwd_fim_classical(R; A)  )
BY
{ (Unfold `bar_bwd_fim_classical` 0 THEN Auto) }


\mforall{}R,A:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.    (bar\_bwd\_fim\_classical(R;  A)  \mmember{}  \mBbbP{})


By

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



Home Index