proposition: Lemma htrans_htrans {x y} : htrans x -> y ∈ x -> htrans y.
proof: Proof. intros [H1 H2] H. split; try now apply H2. intros z Hz. apply H2. now apply (H1 y). Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts FST) Undecidability.FOL(Sets.FST) Undecidability.FOL.TRAKHTENBROT(hfs) Undecidability.Shared.Libs.DLW.Utils(finite) Undecidability(Shared.ListAutomation) Coq(Lia)