proposition: Lemma head_at_l_zero_nil : forall h, head_at_l h (0::nil) = true -> {h' : Hydrae | h = (hcons head h')} + {h = (single head)}.
proof: Proof. destruct h. simpl. case h. right;auto. simpl. destruct h0. simpl. discriminate 1. simpl. discriminate 1. simpl. case h. simpl. left; exists h0;auto. simpl. intros. case (head_at_l_nil _ H). Qed.
imports: Arith Omega List EPSILON0 MSE0