proposition: Lemma satA (M:cmodel) (w:M) C : (forall s, s \in C -> eval (interp s) w) <-> eval [af C] w.
proof: Proof. case: C => xs i /=. change ((forall s, s \in xs -> eval (interp s) w) <-> eval [af xs] w). elim: xs {i} => [|/= s xs IH]. rewrite big_nil forall_nil /=. tauto. rewrite big_cons forall_cons IH {2}/And /=. move: (modelP (interp s) w) (modelP [af xs] w); tauto. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)