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