proposition: Lemma exp_F_eq alpha n : nf alpha -> (exp_F alpha n = alpha ^ n)%t1.
proof: Proof. induction n; cbn. - destruct alpha. + trivial. + destruct alpha1. * destruct n; auto. * trivial. - destruct alpha. intro; now rewrite mult_0_a. destruct alpha1. + destruct n0;auto. intros; assert (alpha2 = zero). { eapply nf_of_finite; eauto. } subst; rewrite mult_1_a. * destruct n;cbn;auto. * apply nf_exp_F. auto with T1. + reflexivity. 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)