proposition: Lemma measure_list_strictly_monotonic : forall l1 l2 (H : one_step_list (one_step rules) l1 l2), (forall t, In t l2 -> well_formed t) -> forall n (P1 P2:Pol_type n), length l2 = n -> monotonic_strict_aux false n P1 P2 -> measure_list l1 n P1 < measure_list l2 n P2.
proof: Proof. intros l1 l2 H Wl2. apply measure_strictly_monotonic_aux; [idtac | assumption | assumption]. intros; apply measure_strictly_monotonic; assumption. Qed.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)