proposition: Lemma uniquize_nil {A beq} (ls : list A) : uniquize beq ls = nil <-> ls = nil.
proof: Proof. induction ls as [|l ls IHls]; simpl. { reflexivity. } { destruct (Equality.list_bin beq l (uniquize beq ls)) eqn:Heq. { apply Equality.list_inA_bl in Heq. rewrite SetoidList.InA_altdef, Exists_exists in Heq. destruct_head ex. destruct_head and. split; intro H'; try congruence. rewrite H' in *; simpl in *. destruct_head False. } { split; congruence. } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts