fact: Fixpoint f_size (s : form) := match s with | fF => 1 | fV p => 1 | fImp s t => (f_size s + f_size t).+1 | fAX s => (f_size s).+1 | fAG s => (f_size s).+1 end.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)