proposition: Lemma length_wf' : forall A len l, length l < len -> Acc (fun l1 l2 : list A => length l1 < length l2) l.
proof: Proof. induction len; simpl; intros; constructor; intros. contradiction (Nat.nlt_0_r _ H). apply IHlen. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT Fiat.ADTNotation Fiat.Computation.FixComp Coq.ZArith.ZArith Coq.Arith.PeanoNat