proposition: Lemma Radd_open (x y : ρ) : forall q q', q < q' -> (∀Z : formula, (∀q'0, x [q'0] → y [q' - q'0] → Z) → Z) ⊆ (∀Z : formula, (∀q'0, x [q'0] → y [q - q'0] → Z) → Z).
proof: Proof. intros. apply Forall_sub_compat. intro. apply sub_Impl; [|reflexivity]. apply Forall_sub_compat. intro. repeat apply sub_Impl; try reflexivity. apply (↓ y). revert H. Qcunfold. lra. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals