proposition: Lemma height_bad : ~ Hvariant Omega free height.
proof: Proof. intros [H]; specialize (H 1 (hyd1 (hyd2 head head)) (hyd1 (hyd1 head))); apply (Nat.lt_irrefl 2), H. - discriminate. - exists 0; right; repeat constructor. Qed.
imports: Coq(Arith Lia) hydras(Hydra_Lemmas ON_Generic ON_Omega)