proposition: Theorem sub_stack : forall A B π, π ∈ ‖B‖ -> A ⊆ B -> π ∈ ‖A‖.
proof: Proof. auto. Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults