proposition: Lemma BuildArgNames_args_name_ok : forall n m, forallb NameDecoration.is_good_varname (BuildArgNames n m) = true.
proof: Proof. intros; eapply forallb_forall; intros. unfold BuildArgNames in H; apply in_app_or in H; intuition; try rewrite <- in_rev in *; apply in_map_iff in H0; destruct_ex; intuition; subst; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction