proposition: Theorem wf_R_list_len@{u} (T : Type@{u}) : well_founded (@R_list_len T).
proof: Proof. constructor. intros. refine (@Fix _ _ Nat.wf_R_lt (fun n : nat => forall ls : list T, n = length ls -> Acc R_list_len ls) (fun x rec ls pfls => Acc_intro _ _) _ _ refl_equal). refine ( match ls as ls return x = length ls -> forall z : list T, R_list_len z ls -> Acc R_list_len z with | nil => fun (pfls : x = 0) z pf => _ | cons l ls => fun pfls z pf => rec _ (match pf in R_list_len xs ys return x = length ys -> Nat.R_nat_lt (length xs) x with | R_l_len n m pf' => fun pf_eq => match eq_sym pf_eq in _ = x return Nat.R_nat_lt (length n) x with | refl_equal => Nat.R_lt pf' end end pfls) _ eq_refl end pfls). clear - pf; abstract (inversion pf; subst; simpl in *; inversion H). Defined.
imports: Coq.Lists.List ExtLib.Core.RelDec ExtLib.Structures.Monoid ExtLib.Structures.Reducible ExtLib.Tactics.Consider ExtLib.Tactics.Injection ExtLib.Structures.Traversable ExtLib.Structures.Functor ExtLib.Structures.Monads ExtLib.Structures.Applicative