proposition: Lemma relativize1 : forall A t, (forall e, t↓e ⊩ ∀x, A x) -> forall e, (λ"Tx" λ"Cx" t)↓e ⊩ ∀₁x∈ℝ, A x.
proof: Proof. intros A t Ht e. start. apply Ht. now find. Qed.
imports: ClassicalRealizability.Kbase ClassicalRealizability.Rationals