proposition: Lemma size_ssub (s : form) (b : bool) : size (ssub (s,b)) <= f_size s.
proof: Proof. elim: s b => //= [|p|s IHs t IHt|s IHs] b; try by rewrite fsetU0 fset1Es. - apply: leq_trans (fsizeU1 _ _) _. apply: leq_ltn_trans (fsizeU _ _) _. rewrite ltnS. exact: leq_add. - apply: leq_trans (fsizeU1 _ _) _. by rewrite ltnS. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)