proposition: Lemma limit_no_head : forall alpha, nf alpha -> T1limit alpha = true -> ~ mem_head (iotas alpha).
proof: Proof. induction alpha. - discriminate. - intros; simpl; destruct (T1limit_cases H). + auto. + destruct a; subst; intro H2; inversion H2. destruct alpha1. * destruct H1;auto. * discriminate H4. * destruct (mem_head_mult_inv _ _ _ H4). destruct alpha1. { destruct H1; auto. } discriminate H6. inversion H6. + intro H7; change (hcons (iota alpha1) (hcons_mult (iota alpha1) n (iotas alpha2))) with (hcons_mult (iota alpha1) (S n) (iotas alpha2)) in H7. destruct (mem_head_mult_inv _ _ _ H7). * destruct alpha1. destruct a. destruct H2;auto. discriminate. * destruct IHalpha2; eauto with T1. tauto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )