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