proposition: Lemma list_sub_wf : LibWf.wf list_sub.
proof: Proof. Proof using. intros l. induction l; apply Acc_intro; introv H. { inverts~ H. } { inverts~ H. applys~ IHl. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)