proposition: Lemma sub_mapsto : forall A c, A ⊆ c ↦ A.
proof: Proof. now intros ? ? ? []. Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults