proposition: Lemma inter_mapsto_distr : forall c A B, c ↦ (A ∩ B) ≈ (c ↦ A) ∩ (c ↦ B).
proof: Proof. intros c A B s. split; intro Hπ. destruct Hπ as [Hc [Hπ | Hπ]]. now left; split. now right; split. destruct Hπ as [[Hc Hπ] | [Hc Hπ]]. now split; try left. now split; try right. Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults