proposition: Theorem paradox : forall P:Prop, P.
proof: Proof. intros P. Generic.paradox h. + exact Type1. + exact (fun X => X). + cbn. exact (fun u F => forall x, F x). + cbn. exact (fun _ _ x => x). + cbn. exact (fun _ _ x => x). + exact (fun F => forall A:Prop, F(up A)). + cbn. exact (fun F f A => f (up A)). + cbn. intros F f A. specialize (f (down A)). rewrite up_down in f. exact f. + exact Prop. + cbn. exact (fun X => X). + cbn. exact (fun A P => forall x:A, P x). + cbn. exact (fun A P => forall x:A, P x). + cbn. exact P. + exact h. + cbn. easy. + cbn. intros F f A. destruct (up_down A). cbn. reflexivity. + cbn. exact (fun _ _ x => x). + cbn. exact (fun _ _ x => x). + cbn. exact (fun _ _ x => x). + cbn. exact (fun _ _ x => x). Qed.