proposition: Lemma satU1P (M : fmodel) (w : M) s C : reflect (evalb (interp s) w /\ satC w C) (satC w (s |` C)).
proof: Proof. rewrite satC1. exact: andP. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.Kstar(Kstar_def)