proposition: Theorem FStalCorrectIncl : forall (Ar : rArray vM) (S : State) (L1 L2 : list triplet) (M : mbDT), incl L1 L2 -> FStalCorrect Ar L1 S M -> FStalCorrect Ar L2 S M.
proof: Proof. intros Ar S L1 L2 M; case M; unfold FStalCorrect in |- *; simpl in |- *; auto with stalmarck. intros Ar' b'; case b'; auto with stalmarck. intros H' t H'0 H'1 H'2 H'3. elim H'1; [ intros S' E; elim E; intros H'6 H'7; elim H'7; intros H'8 H'9; clear H'7 E H'1 | clear H'1 | clear H'1 ]; auto with stalmarck. exists S'; repeat (split; auto with stalmarck). apply stalmarckInclList with (L1 := L1); auto with stalmarck. intros l t H' H'0 H'1 H'2. elim H'0; [ intros H'5 H'6; elim H'6; intros H'7 H'8; elim H'8; intros H'9 H'10; clear H'8 H'6 H'0 | clear H'0 | clear H'0 ]; auto with stalmarck. elim H'7; intros S' E; elim E; intros H'0 H'3; elim H'3; intros H'4 H'6; clear H'3 E H'7; auto with stalmarck. repeat (split; auto with stalmarck). exists S'; repeat (split; auto with stalmarck). apply stalmarckInclList with (L1 := L1); auto with stalmarck. Qed.