proposition: Lemma gE0_eq_intro a b : cnf a = cnf b -> a = b.
proof: Proof. destruct a, b; cbn. move => H; subst => //; congr mkE0; apply eq_proofs_unicity_on; decide equality. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)