fact: Definition satA (M: fmodel) (w:M) a := match a with | aAG (s,H) => hist H s w | aAXG (s,H) => exists2 v, ftrans w v & hist H s v | aVoid => True end.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.Kstar(Kstar_def)