proposition: Lemma phi0_eq_bad : forall alpha, T1omega ^ alpha = phi0 alpha.
proof: Proof. intro alpha. Fail reflexivity. Abort. Lemma phi0_eq : forall alpha, nf alpha -> T1omega ^ alpha = phi0 alpha. Proof. simple induction alpha; cbn. - reflexivity. - destruct alpha0; cbn. + intros H n t H0 H1; generalize (nf_of_finite H1); intro; subst; case n; cbn. * reflexivity. * induction n0; cbn. reflexivity. rewrite IHn0; reflexivity. + intros H n0 t H0 H1; unfold omega_term; rewrite H0; cbn. rewrite <- (omega_term_plus_rw H1); rewrite phi0_plus_mult. 1-2: unfold omega_term. 3-4: eapply nf_inv2; eauto. * auto. * apply single_nf. eauto with T1. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)