proposition: Lemma funsat1 (M : fmodel) C C1 a : (forall w:M, satC w C -> satC w C1) -> funsat M (C1,a) -> funsat M (C,a).
proof: Proof. move => H U [w] [/= /H w1 w2]. apply U. by exists w. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.Kstar(Kstar_def)