proposition: Theorem dilemma1RRLCorrect : forall (f : list rZ -> rArray vM -> _) (Lt : list rZ) (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 (dilemma1RRL f Lt n1 Ar).
proof: Proof. intros f Lt n1 Ar S H'; unfold dilemma1RRL in |- *. generalize (doTripletFsNCorrect getT LL getTCorrect n1 Ar Lt S). case (doTripletsN getT Lt n1 Ar); auto with stalmarck. intros Ar1 b1 L1 T1; case b1; auto with stalmarck. intros H'0. generalize (fun S : State => dilemma1RRCorrect f n1 Ar1 S H'). case (dilemma1RR f n1 Ar1); auto with stalmarck. intros r b l t H'1. apply FStalCorrectComp with (Ar' := Ar1); auto with stalmarck. Qed.