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