proposition: Lemma phi_to_psi : forall alpha beta, {alpha' : T2 & {beta' : T2 | phi alpha beta = [alpha', beta']}}.
proof: Proof. destruct beta; cbn. - now exists alpha, zero. - 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). now exists alpha, (gcons beta1 beta2 0 [zero, zero]). now exists alpha, (gcons beta1 beta2 0 zero). now exists alpha, (gcons beta1 beta2 0 [zero, zero]). now exists alpha, (gcons beta1 beta2 0 (gcons zero zero 0 (gcons t1 t2 n0 t3))). ** destruct t. case (compare alpha beta1). now exists alpha, (gcons beta1 beta2 0 (gcons zero zero (S n0) zero)). now exists alpha, (gcons beta1 beta2 0 (fin (S n0))). now exists alpha, (gcons beta1 beta2 0 (gcons zero zero (S n0) zero)). now exists alpha, (gcons beta1 beta2 0 (gcons zero zero (S n0) (gcons t1 t2 n1 t3))). ++ intros n1 t; now exists alpha, (gcons beta1 beta2 0 (gcons zero (gcons t1 t2 n0 t3) n1 t)). -- exists alpha; exists (gcons beta1 beta2 0 (gcons (gcons t1 t2 n0 t3) t n1 t0)); reflexivity. + intro n0; now exists alpha; exists (gcons beta1 beta2 (S n0) beta3). Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)