proposition: Lemma ret_NIn_BuildArgNames : forall n m, negb (is_in "ret" (BuildArgNames n m)) = true.
proof: Proof. intros. apply Bool.negb_true_iff. apply FacadeFacts.not_is_in_iff. intro. apply in_app_or in H; rewrite <- !in_rev in H; intuition; apply in_map_iff in H0. destruct_ex; intuition; unfold nthArgName in H0; discriminate. destruct_ex; intuition; unfold nthArgName in H0; discriminate. 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