proposition: Lemma order_pred_incl : forall A B, order (@rel_incl A B).
proof: Proof. Proof using. hint refl_rel_incl, antisym_rel_incl, trans_rel_incl. constructors*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)