proposition: Lemma wf_of_rel_incl : forall A (R1 R2 : binary A), wf R1 -> rel_incl R2 R1 -> wf R2.
proof: Proof. Proof using. introv W1 Inc. intros x. pattern x. apply (well_founded_ind W1). clear x. intros x IH. constructor. intros. apply IH. apply~ Inc. Qed.
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)