proposition: Lemma mapsto_sub_compat : forall (c c' : Prop) A B, (c' -> c) -> A ⊆ B -> c ↦ A ⊆ c' ↦ B.
proof: Proof. intros c c' A B Hcs HAB π [Hc Hπ]. split. now apply Hcs. now apply HAB. Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults