proposition: Theorem Σ2_ΣSSn1_correct A : (forall x, In x (fol_vars A) -> R (φ x) (ψ x)) -> fol_sem M2 φ A <-> fol_sem MSSn1 ψ (Σ2_ΣSSn1 d A).
proof: Proof. Proof using All. revert d φ ψ H2 H3. induction A as [ | [] v | b A HA B HB | [] A HA ]; intros d φ ψ H2 H3 H. + simpl; tauto. + simpl in v; revert H. vec split v with x1; vec split v with x2; vec nil v; clear v. revert x1 x2; intros [ x1 | [] ] [ x2 | [] ] H; simpl in H. unfold Q in H1; simpl fol_sem at 1. rewrite H1. 2-3: apply H; auto. unfold P, f; simpl. apply fol_equiv_ext; do 5 f_equal. apply vec_pos_ext; intro p. rewrite vec_pos_map; rew vec. + simpl; apply (fol_bin_sem_ext _). * apply HA; auto; intros; apply H, in_app_iff; auto. * apply HB; auto; intros; apply H, in_app_iff; auto. + simpl; split. * intros (x & Hx). destruct (H2 x) as (y & Hy1 & Hy2). exists y; split; auto. - revert Hy2; unfold P, f; simpl. apply fol_equiv_ext; do 5 f_equal. apply vec_pos_ext; intro p. rewrite vec_pos_map; rew vec. - revert Hx; apply HA; simpl; auto. intros [|i] Hi; simpl; auto. apply H; simpl; apply in_flat_map. exists (S i); simpl; auto. * intros (y & G1 & G2). destruct (H3 y) as (x & Hx). - revert G1; unfold P, f; simpl. apply fol_equiv_ext; do 5 f_equal. apply vec_pos_ext; intro p. rewrite vec_pos_map; rew vec. - exists x; revert G2; apply HA; simpl; auto. intros [|i] Hi; simpl; auto. apply H; simpl; apply in_flat_map. exists (S i); simpl; auto. + simpl; split. * intros G y Hy. destruct (H3 y) as (x & Hx). - revert Hy; unfold P, f; simpl. apply fol_equiv_ext; do 5 f_equal. apply vec_pos_ext; intro p. rewrite vec_pos_map; rew vec. - generalize (G x); apply HA; simpl; auto. intros [|i] Hi; simpl; auto. apply H; simpl; apply in_flat_map. exists (S i); simpl; auto. * intros G x. destruct (H2 x) as (y & Hy1 & Hy2). specialize (G y). spec in G. - revert Hy2; unfold P, f; simpl. apply fol_equiv_ext; do 5 f_equal. apply vec_pos_ext; intro p. rewrite vec_pos_map; rew vec. - revert G; apply HA; simpl; auto. intros [|i] Hi; simpl; auto. apply H; simpl; apply in_flat_map. exists (S i); simpl; auto. Qed.
imports: List Arith Bool Lia Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic fo_sat)