proposition: Lemma eqtype_subtype : forall A B, A ≈ B -> A ⊆ B.
proof: Proof. intros. rewrite H. reflexivity. Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults