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