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