proposition: Lemma succ_ref: refines1 T1.succ T1succ.
proof: Proof. elim => [// |// x] => //; by case: x => // ? ? ? ? ? ? /= -> . Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)