proposition: Lemma mapsto_idempotent : forall c A, c ↦ c ↦ A ≈ c ↦ A.
proof: Proof. intros. apply subtype_eqtype. now intros ? []; repeat split. apply sub_mapsto. Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults