proposition: Lemma measure_bounded : forall t, A0 <= measure t.
proof: Proof. fix measure_bounded 1. intros [a | f l]. simpl. apply Aop.(le_refl). unfold measure. generalize (All_bounded f). unfold bounded. set (f_pol := Pols f). clearbody f_pol. revert f_pol. generalize (get_arity f). revert l . fix measure_bounded_list 1. intros [|t l]. intros [|n]. intros a. simpl. intros p;exact p. intros _ _;apply Aop.(le_refl). intros [|n] f_pol Hb. apply Aop.(le_refl). simpl in f_pol,Hb|-. apply measure_bounded_list. apply Hb. apply measure_bounded. Qed.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)