fact: Fixpoint supp (L : clause) u b := match u,b with | fImp s t,true => supp L s false || supp L t true | fImp s t,false => supp L s true && supp L t false | fAU s t,true => supp L t true || supp L s true && ((fAX (fAU s t),true) \in L) | fAU s t,false => supp L t false && (supp L s false || ((fAX (fAU s t),false) \in L)) | fAR s t,true => supp L t true && (supp L s true || ((fAX (fAR s t),true) \in L)) | fAR s t,false => supp L t false || supp L s false && ((fAX (fAR s t), false) \in L) | _,_ => (u,b) \in L end.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)