proposition: Lemma filter_enumerate {A} {HE : Enumerable A} P a (H : List.filter P (enumerate A) = a::nil) : (forall a', is_true (P a') <-> a = a').
proof: Proof. intro a'; split; intros; assert (H' : In a' (filter P (enumerate A)) <-> In a' (a::nil)) by (rewrite H; reflexivity); clear H; subst; simpl in *; rewrite filter_In in H'; split_iff; split_and; repeat match goal with | [ H : _ \/ False -> _ |- _ ] => specialize (fun k => H (or_introl k)) | [ H : _ /\ _ -> _ |- _ ] => specialize (fun a b => H (conj a b)) | _ => progress specialize_by (apply enumerate_correct) | _ => progress specialize_by assumption | _ => progress specialize_by (exact eq_refl) | _ => progress destruct_head or | _ => progress destruct_head False | _ => assumption end. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.StringFacts Fiat.Common.Equality Fiat.Common