proposition: Theorem sub_id : forall A B, A ⊆ B -> forall e, Id↓e ⊩ A → B.
proof: Proof. intros ? ? H. Ksolve. now apply H. Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults