fact: Fixpoint sat (rho : env domain) (phi : form) : Prop := match phi with | atom P v => eval_predicate rho P (Vector.map (eval rho) v) | fal => False | bin Impl phi psi => sat rho phi -> sat rho psi | bin Conj phi psi => sat rho phi /\ sat rho psi | bin Disj phi psi => sat rho phi \/ sat rho psi | quant_indi Ex phi => exists d : domain, sat ⟨d .: get_indi rho, get_func rho, get_pred rho⟩ phi | quant_indi All phi => forall d : domain, sat ⟨d .: get_indi rho, get_func rho, get_pred rho⟩ phi | quant_func Ex ar phi => exists (f : vec domain ar -> domain), sat ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ phi | quant_func All ar phi => forall (f : vec domain ar -> domain), sat ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ phi | quant_pred Ex ar phi => exists (P : vec domain ar -> Prop), sat ⟨get_indi rho, get_func rho, P .: get_pred rho⟩ phi | quant_pred All ar phi => forall (P : vec domain ar -> Prop), sat ⟨get_indi rho, get_func rho, P .: get_pred rho⟩ phi end.
imports: Vector Arith