proposition: Lemma sat_to_falsity_compat {ff2} rho (phi : @form _ _ _ ff2) : (sat rho default -> False) -> sat rho phi <-> sat rho (phi[default /⊥]).
proof: Proof. induction phi as [|t1 t2|ff [] phi IHphi psi IHpsi|ff [] phi IHphi] in rho,default|-*; intros Hdefault; split. - intros []. - apply Hdefault. - intros H; apply H. - intros H; apply H. - intros H H1. cbn in H. apply IHpsi. 1:easy. apply H. now eapply IHphi, H1. - intros H H1. cbn in H. apply IHpsi with default. 1:easy. apply H. now apply IHphi. - intros H d. apply IHphi. 2: apply H. intros Hd. apply Hdefault. eapply sat_comp in Hd. eapply sat_ext in Hd. 1: apply Hd. now intros [|x]. - intros H d. apply IHphi with (default [↑]). 2: apply H. intros Hd. apply Hdefault. eapply sat_comp in Hd. eapply sat_ext in Hd. 1: apply Hd. now intros [|x]. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability(Shared.ListAutomation) Vector Lia