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