proposition: Lemma cnf_phi0 (alpha : E0) : cnf (E0_phi0 alpha) = T1.phi0 (cnf alpha).
proof: Proof. unfold E0_phi0. now rewrite cnf_rw. Defined.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)