proposition: Lemma gE0lt_wf : well_founded E0lt.
proof: Proof. move => ?; apply Acc_incl with (fun x y => hE0lt (E0_g2h x) (E0_g2h y)). - move => a b ; rewrite /E0lt => Hab. case: a Hab => cnf0 i0 Hb. case: b Hb => cnf1 i1 /= Hlt ; rewrite /E0.E0lt => /=. move: Hlt i0 i1; rewrite -(h2g_g2hK cnf0). rewrite -(h2g_g2hK cnf1) -decide_hltE; repeat split. + move: i0 i1; rewrite -!nf_ref => i0 i1; rewrite g2h_h2gK => //. red. move: i0 => /eqP. by []. + red in Hlt; move: Hlt; rewrite bool_decide_eq_true => //. by rewrite !g2h_h2gK. + move: i1; rewrite -!nf_ref g2h_h2gK /eqP => i1 //. by move: i1 => /eqP. - apply Acc_inverse_image, E0lt_wf. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0) Coq(Relations Basics Wellfounded.Inverse_Image Wellfounded.Inclusion)