proposition: Theorem stalNCorrect : forall (L : list rZ) (n1 m : nat) (Ar : rArray vM) (S : State), FStalCorrect Ar LL S (stalN L n1 m Ar).
proof: Proof. intros L n1 m; generalize n1 L; elim m; simpl in |- *; auto with stalmarck; clear n1 L. intros n1 L Ar S; generalize (dilemmaNCorrect getT LL getTCorrect n L n n1 Ar). case (dilemmaN getT n L n n1 Ar); auto with stalmarck. intros Ar1 b1 L1 T1; case b1; auto with stalmarck. intros n0 H' n1 L Ar S0. generalize (dilemmaNCorrect getT LL getTCorrect n L n n1 Ar). case (dilemmaN getT n L n n1 Ar); auto with stalmarck. intros Ar1 b1 L1 T1; case b1; auto with stalmarck. intros H'0. generalize (H' (S n1) nil Ar1). case (stalN nil (S n1) n0 Ar1). intros r b l t H'1. apply FStalCorrectComp with (Ar' := Ar1); auto with stalmarck. Qed.