proposition: Theorem FStalCorrect0 : forall (Ar : rArray vM) (S : State), FStalCorrect Ar LL S (quatuor (rArray vM) bool (list rZ) Trace Ar false nil emptyTrace).
proof: Proof. intros Ar S; repeat (split; auto with stalmarck). exists S; repeat (split; auto with stalmarck). red in |- *; apply OlistNil; auto with stalmarck. Qed.