empty not in empty, but all in all

all_in_all.v

Require Import Utf8_core Program.Tactics.
Set Universe Polymorphism.

Record Empty := {
  empty :> Type;
  emptiness : ∀ x : empty, False
}.

Program Definition false : Empty := {|
  empty := False
|}.

(* empty not in empty *)

Record Everything := {
  thing :> Type;
}.

Program Definition All : Everything := {|
  thing := Everything
|}.

(* but all in all *)
Check (All : All).