proposition: Lemma head_at_O_cons : forall h l p, head_at h (0::p::l) = true -> {h0:Hydra & {h' : Hydrae | h = node (hcons h0 h') /\ head_at h0 (p::l) = true}} + {h0:Hydra | h = node (single h0) /\ head_at h0 (p::l) = true}.
proof: Proof. destruct h. simpl. discriminate 1. case h. simpl. right. exists h0. auto. simpl. left. exists h0;exists h1;auto. Qed.
imports: Arith Omega List EPSILON0 MSE0