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