fact: Fixpoint height (h:Hydra) : nat := match h with | node l => lheight l end with lheight l : nat := match l with | hnil => 0 | hcons h hs => Nat.max (S (height h)) (lheight hs) end.
imports: hydras(T1 Epsilon0) Coq(List)