proposition: Lemma NoDup_is_no_dup : forall l, NoDup l -> ListFacts3.is_no_dup l = true.
proof: Proof. induction l; simpl; intros. - reflexivity. - inversion H; subst. apply Bool.andb_true_iff; split; eauto. apply forallb_forall; intros. unfold ListFacts3.string_bool; destruct (string_dec x a); subst; simpl; eauto. 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