proposition: Lemma E0_h2g_g2hK : cancel E0_g2h E0_h2g.
proof: Proof. case => a Ha /=; rewrite /E0_g2h /E0_h2g. apply gE0_eq_intro=> /=; by rewrite h2g_g2hK. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)