proposition: Lemma dom_listable h : listable (dom h).
proof: Proof. exists (dom_list h). intros x. induction h as [|[l[[l1|][l2|]]]]; cbn. - destruct x as [x Hx]. apply squash_iff in Hx. apply Hx. - destruct x as [x Hx]. pose proof (proj1 (squash_iff _) Hx) as [H|H]; try discriminate. apply in_map_iff. exists (loc2dom H). split; try apply IHh. now apply dom_eq. - destruct x as [x Hx]. pose proof (proj1 (squash_iff _) Hx) as [H|H]; try discriminate. apply in_map_iff. exists (loc2dom H). split; try apply IHh. now apply dom_eq. - destruct x as [x Hx]. pose proof (proj1 (squash_iff _) Hx) as [H|H]; try discriminate. apply in_map_iff. exists (loc2dom H). split; try apply IHh. now apply dom_eq. - destruct x as [x Hx]. pose proof (proj1 (squash_iff _) Hx) as [H|H]. + left. apply dom_eq. cbn. congruence. + right. apply in_map_iff. exists (loc2dom H). split; try apply IHh. now apply dom_eq. Qed.
imports: Undecidability.FOL(Semantics.FiniteTarski.Full) Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.SeparationLogic(MSL) Undecidability.Shared(Dec) Undecidability.Synthetic.DecidabilityFacts List