proposition: Lemma is_cn_mut : (forall s, is_cnf (cnf s)) * (forall p b, is_cnp (cnp b p)).
proof: Proof. apply: form_prog_rect => //= *; try (case: ifP => //= ?); exact/andP. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)