proposition: Lemma succ_injective : forall alpha (H:nf alpha) beta (H' : nf beta), succ alpha = succ beta -> alpha = beta.
proof: Proof. intros alpha Ha beta Hb Hsucc. destruct (lt_eq_lt_dec alpha beta) as [[H | Heq] | H]. 1,3:apply succ_monomorphism in H; auto; rewrite Hsucc in H; now apply lt_irrefl in H. assumption. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)