proposition: Lemma FL_size : (forall s : form, size (FL s) <= sizef s) * (forall a s, size (FL0 a s) <= sizep a).
proof: Proof. apply: form_prog_ind => /=; try solve [move => *;ssrlia]. - move => s IHs t IHt. rewrite !(leqRW fsizeU). by ssrlia. - move => p IHp s IHs. rewrite (leqRW fsizeU) (leqRW IHs) (leqRW (IHp _)). by ssrlia. - move => a IHa b IHb s. rewrite !(leqRW fsizeU) (leqRW (IHa _)) (leqRW (IHb _)). by ssrlia. - move => a IHa b IHb s. rewrite !(leqRW fsizeU) (leqRW (IHa _)) (leqRW (IHb _)). by ssrlia. - move => p IHp s. apply: leq_trans (fsizeU1 _ _) _. by rewrite !addn1 ltnS. - move => s IHs t. rewrite !(leqRW fsizeU) (leqRW IHs). by ssrlia. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)