proposition: Theorem L_correct a : L_spec (cnf a) (L_ a).
proof: Proof. apply (L_alpha.L_correct (E0_g2h a)). Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder) hydras(T1 E0) hydras(L_alpha) gaia_hydras(T1Bridge GCanon GPaths GHprime)