proposition: Theorem dilemmaNCorrect : forall (L : list rZ) (m n : nat) (Ar : rArray vM) (S : State), FStalCorrect Ar LL S (dilemmaN L m n Ar).
proof: Proof. intros L m n0; generalize L; elim n0; auto with stalmarck; clear L. intros L Ar S; change (FStalCorrect Ar LL S (doTripletsN getT L m Ar)) in |- *. apply doTripletFsNCorrect; auto with stalmarck. intros n1 H' L Ar S0; simpl in |- *; auto with stalmarck. apply dilemma1RRLCorrect; auto with stalmarck. Qed.