proposition: Lemma L2 : gamma = alpha.
proof: Proof. destruct (lt_eq_lt_dec gamma alpha) as [[Hlt | Heq] | Hgt]; [ exfalso|trivial|exfalso]; destruct Halphabeta as [H0 H1]; destruct Hgammaalpha as [H2 H3]; eauto. Qed.
imports: hydras(OrdinalNotations.ON_Generic) Coq(Relations)