proposition: Lemma head_at_l_O_cons : forall h l p, head_at_l h (0::p::l) = true -> {h0:Hydra & {h' : Hydrae | h = (hcons h0 h') /\ head_at h0 (p::l) = true}} + {h0:Hydra | h = (single h0) /\ head_at h0 (p::l) = true}.
proof: Proof. destruct h. simpl. case h. simpl. discriminate 1. right. exists (node h0);auto. left. exists h. exists h0. split;auto. Qed.
imports: Arith Omega List EPSILON0 MSE0