proposition: Lemma sub_inter_r : forall A B, A ∩ B ⊆ B.
proof: Proof. intros. now right. Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults