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