proposition: Lemma Fbis_open (x : Qc -> formula) : forall q q', q < q' -> (∀Z, (∀q'', q' <= q'' ↦ x q'' → Z) → Z) ⊆ (∀Z, (∀q'', q <= q'' ↦ x q'' → Z) → Z).
proof: Proof. intros ? ? Hlt. apply Forall_sub_compat. intro. apply sub_Impl; [| reflexivity]. apply Forall_sub_compat. intro. apply mapsto_sub_compat; [| reflexivity]. revert Hlt. Qcunfold. lra. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals