Commit 7c74cf0c authored by Gregory Malecha's avatar Gregory Malecha
Browse files

A test case.

parent 9b4c31f9
Pipeline #63928 canceled with stage
in 2 minutes and 43 seconds
......@@ -47,3 +47,7 @@ as the types inside of [t] because [tele_arg t]
is essentially just a (dependent) product.
*)
Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t.
Lemma texist_exist_universes (X : Type) (P : TeleS (fun _ : X => TeleO) -> Prop) :
texist P <-> ex P.
Proof. by rewrite texist_exist. Qed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment