proposition: Lemma Hydra_answers : forall h u n, h <> head -> head_at h u = true -> {h':Hydra & Rh n u h h'}.
proof: Proof. intro h; elim h using Hydra_rect2 with (P0 := fun hs => hs <> (single head) -> forall u n, head_at_l hs u = true -> {h':Hydrae & Sh n u hs h'}). intros; absurd (head=head);auto. destruct u. simpl. intros. case (head_at_l_nil _ H1). case u. case n. intros. case (head_at_zero_nil _ H1). destruct 1. injection e. intros; subst h0. exists (node x). left. constructor. constructor. injection 1. intro; subst h0. exists head. left. constructor . intros. case (head_at_S_nil _ _ H1). destruct 1. case a. intros. injection H2. intro; subst h0. assert( hcons x0 x <> single head). discriminate. case (H H4 (S n0::nil) n1 H1). intros;exists (node x1). case s. left. constructor;auto. right. left;auto. right;auto. right;auto. case n. intros. simpl in H1. case (head_at_l_O_cons _ _ _ H1). destruct 1. case s. destruct 1. assert (h0 <> single head). rewrite H2;discriminate. case (H H4 (0::n0::l) n1 H1). intro x1;exists (node x1). case s0. left; constructor. auto. right;left. auto. right. right. auto. destruct 1. case a;intros. clear a. subst h0. assert (single x <> single head). red; intro. injection H2;intro; subst x. simpl in H1. discriminate H1. case (H H2 (0::n0::l) n1). auto. intros;exists (node x0). case s. left;constructor. auto. right;left. auto. right;right. auto. simpl. intros. assert( h0 <> single head). red;intro; subst h0. discriminate H1. case (H H2 _ n2 H1). intros; exists (node x). case s. left;auto. constructor;auto. right;left;auto. right;right. auto. destruct u. simpl. discriminate 1. destruct n. simpl. assert (h0 <> head). red;intro;apply H0;subst h0;auto. intros. case (H u n H1 H2). destruct 1. exists (replicate h' n (single h')). constructor 2. constructor. auto. exists (single h'). constructor 3. constructor;auto. simpl. discriminate 1. destruct u. intros. case (head_at_l_nil _ H2). case n. simpl. case u. intros. assert (h0=head). apply head_at_nil. auto. subst h0. exists h1. constructor 1;constructor. destruct n0. intros. assert (h0 <> head). red;intro;subst h0. discriminate H2. case (H (0::l) n0 H3 H2). destruct 1. exists (replicate h' (S n0) h1). constructor 2. constructor. auto. exists (hcons h' h1). constructor 3. constructor. auto. simpl. intros. assert (h0 <> head). red;intro;subst h0;discriminate H2. case (H (S n0::l) n1 H3 H2). destruct 1. exists (replicate h' (S n1) h1). constructor 2. constructor 2. auto. exists (hcons h' h1). constructor 3. constructor 2. auto. intros. simpl in H2. generalize H2; case n0;case u. simpl. intros. case (head_at_l_zero_nil _ H3). destruct 1. assert (h1 <> single head). rewrite e; discriminate. case (H0 H4 (0::nil) n1). auto. inversion 1. exists (hcons h0 x0). constructor 1. constructor 3. auto. exists (hcons h0 x0). constructor 2. constructor 3. auto. exists (hcons h0 x0). constructor 3. constructor 3. auto. intro H4;subst h1. exists (single h0). constructor 1. constructor. intros. assert (h1 <> single head). intro ; subst h1; discriminate H3. case (H0 H4 (0::n2::l) n1 H3). inversion 1. exists (hcons h0 x). constructor 1. inversion H5. exists (hcons h0 x). constructor 2. constructor 3. auto. exists (hcons h0 x). constructor 3. constructor 3. auto. intros; assert (h1 <> single head). intro; subst h1;discriminate H3. case (H0 H4 (S n2::nil) n1 H3). inversion 1. exists (hcons h0 x). constructor 1. constructor 3. auto. exists (hcons h0 x). constructor 2. constructor 3;auto. exists (hcons h0 x). constructor 3. constructor 3. auto. intros. assert (h1 <> single head). red;intro;subst h1;discriminate H3. case (H0 H4 _ n1 H3). inversion 1. inversion H5. exists (hcons h0 x). constructor 2. constructor 3. auto. exists (hcons h0 x). constructor 3. constructor 3. auto. Defined.
imports: Arith Omega List EPSILON0 MSE0