proposition: Lemma Predecessor_unicity (alpha beta gamma : A): Successor beta alpha -> Successor beta gamma -> gamma = alpha.
proof: Proof. intros H H0. apply (L2 _ _ H _ H0). Qed.
imports: hydras(OrdinalNotations.ON_Generic) Coq(Relations)