proposition: Theorem hfs_comprehension X (P : X -> Prop) (f : X -> hfs) : fin_t P -> { s | forall a, a ∈ s <-> exists x, P x /\ f x = a }.
proof: Proof. intros (l & Hl). assert { s | forall a, a ∈ s <-> exists x, In x l /\ f x = a } as H. { exists (fold_right (fun x => hfs_cons (f x)) hfs_empty l). clear Hl; intros a. induction l as [ | x l IHl ]; simpl. + rewrite hfs_empty_spec; split; try tauto. intros (? & [] & _). + rewrite hfs_cons_spec, IHl; split. * intros [ -> | (y & ? & <-) ]. - exists x; auto. - exists y; auto. * intros (y & [ -> | ? ] & <-); auto. right; exists y; auto. } destruct H as (s & Hs). exists s; intro a; rewrite Hs. fol equiv; intro; rewrite Hl; tauto. Qed.
imports: List Arith Lia Max Wellfounded Setoid Eqdep_dec Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.Shared.Libs.DLW.Wf(wf_finite wf_chains) Undecidability.FOL.TRAKHTENBROT(notations fol_ops membership btree)