proposition: Theorem phi_principalR alpha beta : nf alpha -> nf beta -> {gamma:T2 | [alpha, beta] = phi zero gamma}.
proof: Proof. intros Valpha Vbeta; case (phi_cases' alpha Vbeta). destruct 1. - case s; intros b1 (b2,(H1,(H2,H3))). case (lt_ge_dec zero alpha). intro l; exists [alpha, beta]; cbn. + rewrite (compare_rw_lt l);auto with T2. + intro; assert(alpha = zero). { inversion l;auto with T2. lt_clean. } subst alpha beta; exists (gcons b1 b2 0 (fin 1)). cbn; rewrite (compare_rw_lt H2);auto with T2. - case (lt_ge_dec zero alpha). + exists (phi alpha beta). rewrite phi_spec1;auto with T2. + intro;assert (alpha=zero). case l; auto with T2. intro;lt_clean. subst alpha; exists beta. auto with T2. - intros (b1,(b2,(n,(H1,(H2,H3))))); subst beta. case (lt_ge_dec zero alpha). + intro l; exists [alpha, (gcons b1 b2 0 (fin (S n)))]. cbn; rewrite (compare_rw_lt l). reflexivity. + intro l;assert (alpha=zero). * case l; auto with T2. intro;lt_clean. * subst alpha; exists (gcons b1 b2 0 (fin (S (S n))));cbn; rewrite (compare_rw_lt H2); auto with T2. Defined.
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)