proposition: Lemma sat_comp_i rho σ phi : sat rho (phi[σ]i) <-> sat ⟨σ >> eval rho, get_func rho, get_pred rho⟩ phi.
proof: Proof. induction phi in rho, σ |- *; cbn. - reflexivity. - destruct p; cbn; erewrite map_map, map_ext; try reflexivity; induction t; firstorder using eval_comp_i. - specialize (IHphi1 rho σ); specialize (IHphi2 rho σ). destruct b; cbn; intuition easy. - destruct q. + setoid_rewrite IHphi. split; intros H d; eapply sat_ext. 2, 4: apply (H d). all: clear; intros []; split; try easy; cbn; erewrite eval_comp_i; now destruct rho. + setoid_rewrite IHphi. split; intros [d H]; exists d; eapply sat_ext. 2, 4: apply H. all: clear; intros []; split; try easy; cbn; erewrite eval_comp_i; now destruct rho. - destruct q. + setoid_rewrite IHphi; split; intros H f; eapply sat_ext. 2, 4: apply (H f). all: clear; split; try easy. 2: symmetry. all: apply eval_subst_cons_shift_f. + setoid_rewrite IHphi; split; intros [f H]; exists f; eapply sat_ext. 2, 4: apply H. all: clear; split; try easy. 2: symmetry. all: apply eval_subst_cons_shift_f. - destruct q. + setoid_rewrite IHphi; split; intros H P; eapply sat_ext. 2, 4: apply (H P). all: clear; split; try easy; now apply eval_ext. + setoid_rewrite IHphi; split; intros [P H]; exists P; eapply sat_ext. 2, 4: apply H. all: clear; split; try easy; now apply eval_ext. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector