proposition: Lemma hfs_ax_ind phi rho : rho ⊨ ax_ind phi.
proof: Proof. cbn. intros H1 H2. apply hfs_ind. - apply sat_comp in H1. eapply sat_ext; try apply H1. now intros []. - setoid_rewrite sat_comp in H2. intros x y Hx Hy. eapply sat_ext; try apply (H2 y x). + now intros []. + eapply sat_ext; try apply Hx. now intros []. + eapply sat_ext; try apply Hy. now intros []. 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)