proposition: Lemma phi_to_psi : forall alpha beta, {alpha' : T2 & {beta' : T2 | phi alpha beta = [alpha', beta']}}.
proof: Proof. destruct beta;simpl. exists alpha; exists zero;trivial. case n. case beta3. case (compare alpha beta1). exists alpha;exists [beta1, beta2];trivial. exists beta1;exists beta2;trivial. exists alpha;exists [beta1, beta2];trivial. destruct t. destruct t. destruct n0. destruct t. case (compare alpha beta1). exists alpha;exists (cons beta1 beta2 0 [zero, zero]);trivial. exists alpha;exists (cons beta1 beta2 0 zero);trivial. exists alpha;exists (cons beta1 beta2 0 [zero, zero]);trivial. exists alpha; exists (cons beta1 beta2 0 (cons zero zero 0 (cons t1 t2 n0 t3))); trivial. destruct t. case (compare alpha beta1). exists alpha; exists (cons beta1 beta2 0 (cons zero zero (S n0) zero)). trivial. exists alpha;exists (cons beta1 beta2 0 (F S n0));trivial. exists alpha;exists ( cons beta1 beta2 0 (cons zero zero (S n0) zero));trivial. exists alpha; exists ( cons beta1 beta2 0 (cons zero zero (S n0) (cons t1 t2 n1 t3))); trivial. intros n1 t;exists alpha; exists (cons beta1 beta2 0 (cons zero (cons t1 t2 n0 t3) n1 t));trivial. exists alpha;exists (cons beta1 beta2 0 (cons (cons t1 t2 n0 t3) t n1 t0)); trivial. intro n0;exists alpha;exists (cons beta1 beta2 (S n0) beta3);trivial. 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