proposition: Lemma nf_ref (a: hT1) : T1.nf_b a = T1nf (h2g a).
proof: Proof. elim: a => //. - move => a IHa n b IHb; rewrite T1.nf_b_cons_eq; simpl T1nf. by rewrite IHa IHb [phi0 (h2g a)]/(h2g (T1.phi0 a)) andbA decide_hltE. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)