fact: Definition literal (s : sform) := let: (t,_) := s in match t with | fV _ => true | fAX _ => true | fF => true | _ => false end.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)