proposition: Lemma F_open (x : Qc -> formula) : forall q q', q < q' -> (∀q'0, q'0 <= q' ↦ x q'0) ⊆ (∀q'0, q'0 <= q ↦ x q'0).
proof: Proof. intros ? ? Hlt. apply Forall_sub_compat. intro. apply mapsto_sub_compat. apply Qclt_le_weak in Hlt. now transitivity q. reflexivity. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals