proposition: Lemma FL_cnf_mut : (forall s, is_cnf s -> forall t, t \in FL s -> is_cnf t)* (forall p s, is_cnp p -> is_cnf s -> forall t, t \in FL0 p s -> is_cnf t).
proof: Proof. apply form_prog_rect => /=; intros; repeat (simpl; match goal with | [H : is_true (_ \in [fset _]) |- _] => rewrite inE in H; move/eqP : H => H; subst | [H : is_true (_ \in _ `|` _) |- _] => case/fsetUP : H => H | [H : is_true (_ && _) |- _] => let H' := fresh in case/andP : H => H H' | [H : is_true (_ && _) |- _] => let H' := fresh in case/andP : H => H H' | [ |- is_true (_ && _)] => apply/andP; split end); try auto; try eauto. - apply: (H [p0]s) => //=. by apply/andP; split. - apply: (H [p^*]s) => //=. by apply/andP; split. - destruct p => //. by apply: H. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)