proposition: Theorem dilemma1RRCorrect : forall (f : list rZ -> rArray vM -> _) (n1 : nat) (Ar : rArray vM) (S : State), (forall (L : list rZ) (Ar : rArray vM) (S : State), FStalCorrect Ar LL S (f L Ar)) -> FStalCorrect Ar LL S (dilemma1RR f n1 Ar).
proof: Proof. intros f n1; elim n1; simpl in |- *; auto with stalmarck. intros Ar S H'. generalize (dilemma1RCorrect f n zero Ar S H'). case (dilemma1R f zero n Ar). intros Ar1 b1 L1 T1; case b1; auto with stalmarck. case L1; auto with stalmarck. intros n0 H' Ar S H'0. generalize (dilemma1RCorrect f n zero Ar S H'0). case (dilemma1R f zero n Ar). intros Ar1 b1 L1 T1; case b1; auto with stalmarck. case L1; auto with stalmarck. intros r l H'1. generalize (fun S : State => H' Ar1 S H'0). case (dilemma1RR f n0 Ar1). intros r0 b l0 t H'2. apply FStalCorrectComp with (Ar' := Ar1); auto with stalmarck. Qed.