Prooven No_external_after_switch Lemma

src/semantics/FPBigStepClight.v

@@ -398,7 +398,20 @@ 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.
+Proof. 
+  intros a sl. induction sl; simpl; subst.
+  - intros _ _ . constructor.
+  - intros n NECswitch. destruct o.
+    + unfold select_switch. unfold select_switch_case. destruct (zeq z n).
+      * inversion NECswitch. apply NECSL_NECSseq. apply H0.
+      * apply IHsl. inversion NECswitch. constructor. inversion H0.
+        apply H6.
+    + unfold select_switch.  simpl. destruct (select_switch_case n sl) eqn:SelectRes.
+      * unfold select_switch in IHsl. have IHsln := (IHsl n). 
+        rewrite SelectRes in IHsln. apply IHsln.
+        inversion NECswitch. constructor. inversion H0. apply H6.
+      * inversion NECswitch. apply NECSL_NECSseq. apply H0.  
+Qed.
 
 Inductive No_external_call_cont : cont -> Prop :=
   | NEC_Kstop : No_external_call_cont Kstop