proposition: Theorem paradox : False.
proof: Proof. Generic.paradox p. + exact U. + exact (fun X=>X). + cbn. exact (fun X F => forall x:X, F x). + cbn. exact (fun _ _ x => x). + cbn. exact (fun _ _ x => x). + exact (fun F => forall x:A, F (up x)). + cbn. exact (fun _ f => fun x:A => f (up x)). + cbn. intros * f X. specialize (f (down X)). rewrite up_down in f. exact f. + exact A. + cbn. exact up. + cbn. exact (fun _ F => down (forall x, up (F x))). + cbn. exact (fun _ F => down (forall x, up (F x))). + cbn. exact (down False). + rewrite up_down in p. exact p. + cbn. easy. + cbn. intros ? f X. destruct (up_down X). cbn. reflexivity. + cbn. intros ? ? f. rewrite up_down. exact f. + cbn. intros ? ? f. rewrite up_down in f. exact f. + cbn. intros ? ? f. rewrite up_down. exact f. + cbn. intros ? ? f. rewrite up_down in f. exact f. Qed.