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