proposition: Theorem reln_hfs : { Y : Type & { _ : finite_t Y & { mem : Y -> Y -> Prop & { _ : forall u v, { mem u v } + { ~ mem u v } & { yd : Y & { yr : Y & { i : X -> Y & { s : Y -> X & (forall x, mem (i x) yd) /\ (forall y, mem y yd -> exists x, y = i x) /\ (forall v, R v <-> mb_is_tuple_in mem yr (vec_map i v)) }}}}}}}}.
proof: Proof. Proof using x0 Xfin Xdiscr HR. exists Y, HY, mem, mem_dec, yd, yr, i', s'. msplit 2; auto. + intros y Hy; unfold i'. destruct (Hi' Hy) as (x & Hx). exists x; apply eqY; simpl; auto. + intros v; rewrite Hr3; split. * intros Hv. red. assert (H1 : p_bool (hfs_tuple (vec_map i v)) = true). { apply p_bool_spec, Hp1 with (1 := Hv); auto. } exists (exist _ (hfs_tuple (vec_map i v)) H1); split. - apply is_tuple; simpl; rewrite vec_map_map; auto. - unfold yr; red; simpl; auto. * intros ((t & Ht) & H1 & H2). rewrite is_tuple in H1. simpl in H1, H2. rewrite vec_map_map in H1; subst t; auto. Qed.
imports: List Arith Lia Eqdep_dec Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations decidable fol_ops membership hfs)