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