proposition: Lemma length_wf : forall A, well_founded (fun l1 l2 : list A => length l1 < length l2).
proof: Proof. red; intros; eapply length_wf'; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT Fiat.ADTNotation Fiat.Computation.FixComp Coq.ZArith.ZArith Coq.Arith.PeanoNat