proposition: Lemma succ_ref (alpha : t) : refine (succ alpha) = T1.succ (refine alpha).
proof: Proof. induction alpha. - now cbn. - destruct alpha. + destruct a; cbn; destruct n; now cbn. + destruct a; destruct n. * now cbn. * destruct p; destruct n1. -- now cbn. -- cbn in *; now rewrite IHalpha. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )