proposition: Theorem paradox : forall B:MProp, El B.
proof: Proof. intros B. Generic.paradox h. + exact MProp. + exact El. + exact (fun _ => Forall). + cbn. exact (fun _ _ f => f). + cbn. exact (fun _ _ f => f). + exact Forall. + cbn. exact (fun _ f => f). + cbn. exact (fun _ f => f). + exact bool. + exact (fun b => El (b2p b)). + cbn. exact (fun _ F => p2b (Forall (fun x => b2p (F x)))). + exact (fun _ F => p2b (Forall (fun x => b2p (F x)))). + apply p2b. exact B. + cbn in h. auto. + cbn. easy. + cbn. easy. + cbn. auto. + cbn. intros * f. apply p2p1 in f. cbn in f. exact f. + cbn. auto. + cbn. intros * f. apply p2p1 in f. cbn in f. exact f. Qed.