fact: Fixpoint measure_list (l: list term) : forall n0 : nat, Pol_type n0 -> A := match l with | nil => fun n0 : nat => match n0 as n1 return (Pol_type n1 -> A) with | 0 => fun a : Pol_type 0 => a | S n1 => fun _ : Pol_type (S n1) => A0 end | t0 :: l1 => fun n0 : nat => match n0 as n1 return (Pol_type n1 -> A) with | 0 => fun _ : Pol_type 0 => A0 | S n1 => fun f_pol0 : A -> Pol_type n1 => measure_list l1 n1 (f_pol0 (measure t0)) end end.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)