proposition: Lemma inter_sub_compat : forall A A' B B', A ⊆ A' -> B ⊆ B' -> A ∩ B ⊆ A' ∩ B'.
proof: Proof. intros A A' B B' HA HB ? [? | ?]. now left; apply HA. now right; apply HB. Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults