proposition: Lemma ap_ref : refinesPred Epsilon0.T1.ap T1ap.
proof: Proof. move => a; split => Hap; first by case: Hap. move: Hap; case: a => //= a n b /andP [Hn Hz]. move/eqP: Hn Hz =>->; move/eqP; by case: b. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)