proposition: Lemma BuildArgNamesNoDup n m : ListFacts3.is_no_dup (BuildArgNames n m) = true.
proof: Proof. apply NoDup_is_no_dup; unfold BuildArgNames. apply ListFacts1.NoDup_app; try rewrite <- NoDup_rev. - apply ListFacts1.Injection_NoDup. eapply IsInjection_nthArgName. apply NoDupNumUpTo; simpl; try constructor; intuition. - apply ListFacts1.Injection_NoDup. eapply IsInjection_nthRepName. apply NoDupNumUpTo; simpl; try constructor; intuition. - unfold ListFacts1.Disjoint, not; intros; intuition. rewrite <- in_rev in *. eapply in_map_iff in H0; eapply in_map_iff in H1; destruct_ex; intuition; subst. unfold nthRepName, 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