proposition: Lemma E0g2h_Fin i: E0_g2h (E0fin i) = E0.E0fin i.
proof: Proof. apply E0_eq_intro => /=; rewrite E0fin_cnf; by case: i. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)