proposition: Theorem dilemma1RCorrect : forall (f : list rZ -> rArray vM -> _) (n1 : nat) (v : rNat) (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 (dilemma1R f v n1 Ar).
proof: Proof. intros f n1; elim n1; simpl in |- *; auto with stalmarck. intros v Ar S H'; case (rArrayGet vM Ar v); auto with stalmarck. intros H'0. apply FStalCorrect0; auto with stalmarck. intros L; generalize (dilemma1Correct f Ar (rZPlus v) rZTrue S H'). case (dilemma1 f Ar (rZPlus v) rZTrue). intros Ar1 b1 L1 T1; case b1; auto with stalmarck. intros n0 H' v Ar S H'0. case (rArrayGet vM Ar v); auto with stalmarck. intros L; generalize (dilemma1Correct f Ar (rZPlus v) rZTrue S H'0). case (dilemma1 f Ar (rZPlus v) rZTrue). intros Ar1 b1 L1 T1; case b1; auto with stalmarck. intros H'1. generalize (fun S : State => H' (rnext v) Ar1 S H'0). case (dilemma1R f (rnext v) n0 Ar1). intros r b l t H'2. apply FStalCorrectComp with (Ar' := Ar1); auto with stalmarck. Qed.