proposition: Lemma cnf_eq_mut : (forall (s : form), prv (cnf s <--> s)) /\ (forall (p : prog) (s : form), prv ([cnp true p]s <--> [p^^]s) * prv ([cnp false p]s <--> [p]s)).
proof: Proof. apply: form_prog_ind => /=; intros; try solve [repeat (match goal with | [H : forall _, _ * _ |- _] => first [do ! rewrite -> ((H _).1)|do ! rewrite -> ((H _).2)]; clear H | [H : prv _ |- _] => repeat rewrite -> H; clear H end); exact: ax_eq_refl]. - split; exact: ax_eq_refl. - split. + rewrite -> ax_conv_ch, ax_Ch, ax_Ch. rewrite -> (H _).1, (H0 _).1. exact: ax_eq_refl. + rewrite -> ax_Ch,(H _).2, (H0 _).2. rewrite -> ax_Ch. exact: ax_eq_refl. - split. + rewrite -> ax_Con,ax_conv_con,ax_Con. rewrite -> (H _).1 , (H0 _).1. exact: ax_eq_refl. + rewrite -> ax_Con, ax_Con, (H _).2, (H0 _).2. exact: ax_eq_refl. - split. + rewrite -> ax_conv_star. apply: rStar_eq => {s} - s. exact: (H s).1. + apply: rStar_eq => {s} - s. exact: (H s).2. - split. + rewrite -> ax_conv_test. do ! rewrite -> ax_test. rewrite -> H. exact: ax_eq_refl. + do ! rewrite -> ax_test. rewrite -> H. exact: ax_eq_refl. - split; last exact: (H _).1. rewrite -> ax_conv. exact: (H _).2. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)