fact: Fixpoint sizef (s : form) := match s with | fV p => 1 | fF => 1 | fImp s t => (1 + sizef s + sizef t)%N | [a]s => (1 + sizep a + sizef s)%N end with sizep (a : prog) := match a with | pV a => 1 | a + b => (1 + sizep a + sizep b)%N | a ;; b => (1 + sizep a + sizep b)%N | a^* => (sizep a + 1)%N | t?? => (1 + sizef t)%N end.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)