proposition: Lemma newVar2 : forall (l : list nat) (n : nat), In n l -> n < newVar l.
proof: Proof. induction l as [| a l Hrecl]. - destruct 1. - destruct 1 as [H| H]. + rewrite H; unfold newVar in |- *; simpl in |- *. induction (fold_right Nat.max 0 (map S l)). * apply Nat.lt_succ_diag_r . * apply Nat.lt_succ_r; apply Nat.le_max_l. + unfold newVar in Hrecl |- *; simpl. assert (H0: fold_right Nat.max 0 (map S l) = 0 \/ (exists n : nat, fold_right Nat.max 0 (map S l) = S n)). { induction (fold_right Nat.max 0 (map S l)) as [| n0 IHn0]. - auto. - right; now exists n0. } destruct H0 as [H0| [x0 H0]]. * rewrite H0; rewrite H0 in Hrecl. elim (Nat.nlt_0_r n (Hrecl _ H)). * rewrite H0; rewrite H0 in Hrecl. -- apply Nat.lt_le_trans with (S x0). ++ now apply Hrecl. ++ apply le_n_S, Nat.le_max_r. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)