proposition: Lemma inter_inf : forall (s s' : t) (a : elt) (Hs : Ok s) (Hs' : Ok s'), Inf a s -> Inf a s' -> Inf a (inter s s').
proof: Proof. induction2. - apply Inf_lt with x; auto. - apply Hrec'; auto. apply Inf_lt with x'; auto. Qed.
imports: MSetInterface OrdersFacts OrdersLists