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