proposition: Lemma E0is_succE a: E0is_succ a -> {beta: E0 | a = E0_succ beta}.
proof: Proof. rewrite /E0is_succ => H. case (Succb_Succ _ H) => beta Hbeta; exists (E0_h2g beta). rewrite -(E0_h2g_g2hK a) Hbeta. have H0:= g2h_E0_succ (E0_h2g beta). move: H0; rewrite E0_g2h_h2gK. move => H0; rewrite -H0. by rewrite E0_h2g_g2hK. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)