proposition: Lemma Forall_sub_compat : forall T A B, (forall x : T, A x ⊆ B x) -> (∀x, A x) ⊆ ∀x, B x.
proof: Proof. intros T A B Hsub π [n Hn]. exists n. now apply Hsub. Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults