add some NEC_statement Lemma

src/semantics/FPBigStepClight.v

@@ -382,6 +382,23 @@ with No_external_call_statement_labeled : labeled_statements -> Prop :=
       No_external_call_statement_labeled lst ->
         No_external_call_statement_labeled (LScons l st lst).
 
+Lemma NECSL_NECSseq : forall sl,
+  No_external_call_statement_labeled sl <-> No_external_call_statement (seq_of_labeled_statement sl).
+Proof.
+  intros sl. split; intros H; induction sl.
+  - 
+    + simpl. constructor.
+    + simpl. constructor; inversion H; subst. apply H2. apply (IHsl H4).
+  - 
+    + constructor.
+    + simpl in H. inversion H; subst. constructor; auto.
+Qed.
+
+
+Lemma No_external_after_switch : forall a sl n,
+  No_external_call_statement (Sswitch a sl) ->
+    No_external_call_statement (seq_of_labeled_statement (select_switch n sl)).
+Proof. Admitted.
 
 Axiom No_SBuiltin :
   forall s, No_external_call s.