proposition: Lemma g2h_E0_succ a : E0_g2h (E0_succ a)= E0.E0_succ (E0_g2h a).
proof: Proof. rewrite /E0_succ; apply E0_eq_intro => /=; by rewrite g2h_succ. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)