proposition: Fact fol_quant_sem_ext X q (P Q : X -> Prop) : (forall x, P x <-> Q x) -> fol_quant_sem q P <-> fol_quant_sem q Q.
proof: Proof. revert q; intros [] H; simpl. + split; intros (k & ?); exists k; apply H; auto. + split; intros ? k; apply H; auto. Qed.
imports: List Arith Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_list finite)