proposition: Lemma Beckman_eqtype : forall A : nat -> Prop, prop (forall n, A n) ≈ (∀n, prop (A n)).
proof: Proof. intro A. intros s; split; intro Hs; dec s. + exists 0. left. split. now apply HF. ok. + apply Classical_Pred_Type.not_all_ex_not in HF. destruct HF as [n Hn]. exists n. right. repeat split; ok. + elim (Classical_Prop.classic (forall n, A n)); intro HA. - left. now split. - right. unfold one in Hs. dec s. repeat split; ok. + right. split. intro Habs. elim HF. now apply Habs. split; ok. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping