proposition: Theorem wf_R_string_len : well_founded R_string_len.
proof: Proof. constructor. intros. refine (@Fix _ _ wf_R_lt (fun n : nat => forall ls : string, n = length ls -> Acc R_string_len ls) (fun x rec ls pfls => Acc_intro _ _) _ _ refl_equal). refine ( match ls as ls return x = length ls -> forall z : string, R_string_len z ls -> Acc R_string_len z with | EmptyString => fun (pfls : x = 0) z pf => _ | String l ls => fun pfls z pf => rec _ (match pf in R_string_len xs ys return x = length ys -> R_nat_lt (length xs) x with | R_s_len n m pf' => fun pf_eq => match eq_sym pf_eq in _ = x return R_nat_lt (length n) x with | refl_equal => R_lt pf' end end pfls) _ eq_refl end pfls). clear - pf; abstract (inversion pf; subst; simpl in *; inversion H). Defined.
imports: Coq.Strings.String Coq.Program.Program Coq.Arith.PeanoNat ExtLib.Tactics.Consider ExtLib.Core.RelDec ExtLib.Structures.Reducible ExtLib.Structures.Monoid ExtLib.Data.Char ExtLib.Data.Nat