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