proposition: Theorem doTripletFsRCorrect : forall (Ar : rArray vM) (Lt : list rZ) (S : State), FStalCorrect Ar LL S (doTripletsR Lt Ar).
proof: Proof. intros Ar Lt; generalize Ar; clear Ar; elim Lt; simpl in |- *. exact FStalCorrect0. intros a l H' Ar S; generalize (doTripletFsCorrect Ar (getT a) S). case (doTripletFs (getT a) Ar); auto with stalmarck. intros Ar' b' L' T'; case b'. intros H'0. apply FStalCorrectIncl with (L1 := getT a); auto with stalmarck. generalize (H' Ar'). case (doTripletsR l Ar'). intros r b l0 t H'0 H'1. apply FStalCorrectComp with (Ar' := Ar'); auto with stalmarck. apply FStalCorrectIncl with (L1 := getT a); auto with stalmarck. Qed.