proposition: Lemma phi_of_any_cons : forall alpha beta1 beta2 n gamma, omega <= gamma \/ (0 < n)%nat -> phi alpha (cons beta1 beta2 n gamma) = [alpha, (cons beta1 beta2 n gamma)].
proof: Proof. simpl. intros until n; case n. destruct 1. generalize H; case gamma. destruct 1. discriminate H0. lt_clean. intro t;case t. intro t0;case t0. destruct 1. discriminate H0. inversion H0; lt_clean; auto with T2. auto with T2. auto with T2. lt_clean. auto with T2. Qed.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo