proposition: Lemma NoDup_rev {A} : forall (l : list A), NoDup l <-> NoDup (rev l).
proof: Proof. induction l; simpl; split; eauto. - intros; apply ListFacts1.NoDup_app. + inversion H; subst; eapply IHl; eauto. + repeat econstructor; eauto. + unfold ListFacts1.Disjoint; unfold not; intros. inversion H; subst; apply H3. intuition; inversion H2; subst; eauto. * apply in_rev; auto. * inversion H5. - intros; pose proof (NoDup_remove_1 _ nil a H); pose proof (NoDup_remove_2 _ nil a H). rewrite app_nil_r in *. econstructor. + setoid_rewrite in_rev; eauto. + apply IHl; auto. 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