fact: Definition Oi (i : nat)(s : (State * nat))(a : A) : Comp (B * (State * nat)) := [s_s, s_i] <-2 s; let O_c := if (ge_dec s_i i) then O2 else O1 in [b, s_s'] <-$2 O_c s_s a; ret (b, (s_s', (S s_i))).
imports: FCF.FCF FCF.RndInList