fact: Fixpoint ssub' b s := (s,b) |` match s with | fImp s t => ssub' (negb b) s `|` ssub' b t | fAX t => ssub' b t | fAG s => (fAX (fAG s),b) |` ssub' b s | _ => fset0 end.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)