diff --git a/common/_CoqProject.in b/common/_CoqProject.in
index 66dfd7215..45bccac4f 100644
--- a/common/_CoqProject.in
+++ b/common/_CoqProject.in
@@ -5,6 +5,7 @@ theories/uGraph.v
 theories/config.v
 theories/Kernames.v
 theories/Universes.v
+theories/UniversesDec.v
 theories/BasicAst.v
 theories/Environment.v
 theories/Reflect.v
diff --git a/common/theories/EnvironmentTyping.v b/common/theories/EnvironmentTyping.v
index 687c0cbd5..222105480 100644
--- a/common/theories/EnvironmentTyping.v
+++ b/common/theories/EnvironmentTyping.v
@@ -284,6 +284,19 @@ Module Lookup (T : Term) (E : EnvironmentSig T).
       (fun u => forall l, LevelExprSet.In l u -> LevelSet.In (LevelExpr.get_level l) (global_ext_levels Σ))
       True s.
 
+  Definition wf_universe_dec Σ s : {@wf_universe Σ s} + {~@wf_universe Σ s}.
+  Proof.
+    destruct s; try (left; exact I).
+    cbv [wf_universe Universe.on_sort LevelExprSet.In LevelExprSet.this t_set].
+    destruct t as [[t _] _].
+    induction t as [|t ts [IHt|IHt]]; [ left | | right ].
+    { inversion 1. }
+    { destruct (LevelSetProp.In_dec (LevelExpr.get_level t) (global_ext_levels Σ)) as [H|H]; [ left | right ].
+      { inversion 1; subst; auto. }
+      { intro H'; apply H, H'; now constructor. } }
+    { intro H; apply IHt; intros; apply H; now constructor. }
+  Defined.
+
   Lemma declared_ind_declared_constructors `{cf : checker_flags} {Σ ind mib oib} :
     declared_inductive Σ ind mib oib ->
     Alli (fun i => declared_constructor Σ (ind, i) mib oib) 0 (ind_ctors oib).
diff --git a/common/theories/UniversesDec.v b/common/theories/UniversesDec.v
new file mode 100644
index 000000000..bae647212
--- /dev/null
+++ b/common/theories/UniversesDec.v
@@ -0,0 +1,203 @@
+From MetaCoq.Utils Require Import MCList MCOption MCUtils.
+From MetaCoq.Common Require Import uGraph.
+From MetaCoq.Common Require Import Universes.
+Import wGraph.
+
+Definition levels_of_cs (cstr : ConstraintSet.t) : LevelSet.t
+  := ConstraintSet.fold (fun '(l1, _, l2) acc => LevelSet.add l1 (LevelSet.add l2 acc)) cstr (LevelSet.singleton Level.lzero).
+Lemma levels_of_cs_spec cstr (lvls := levels_of_cs cstr)
+  : uGraph.global_uctx_invariants (lvls, cstr).
+Proof.
+  subst lvls; cbv [levels_of_cs].
+  cbv [uGraph.global_uctx_invariants uGraph.uctx_invariants ConstraintSet.For_all declared_cstr_levels]; cbn [fst snd ContextSet.levels ContextSet.constraints].
+  repeat first [ apply conj
+               | progress intros
+               | progress destruct ?
+               | match goal with
+                 | [ |- ?x \/ ?y ]
+                   => first [ lazymatch x with context[LevelSet.In ?l (LevelSet.singleton ?l)] => idtac end;
+                              left
+                            | lazymatch y with context[LevelSet.In ?l (LevelSet.singleton ?l)] => idtac end;
+                              right ]
+                 | [ H : ConstraintSet.In ?l ?c |- ?x \/ ?y ]
+                   => first [ lazymatch x with context[LevelSet.In _ (ConstraintSet.fold _ c _)] => idtac end;
+                              left
+                            | lazymatch y with context[LevelSet.In _ (ConstraintSet.fold _ c _)] => idtac end;
+                              right ]
+                 end
+               | rewrite !LevelSet.union_spec
+               | progress rewrite <- ?ConstraintSet.elements_spec1, ?InA_In_eq in *
+               | rewrite ConstraintSetProp.fold_spec_right ].
+  all: lazymatch goal with
+       | [ |- LevelSet.In Level.lzero (List.fold_right ?f ?init ?ls) ]
+         => first [ LevelSetDecide.fsetdec
+                  | cut (LevelSet.In Level.lzero init);
+                    [ generalize init; induction ls; intros; cbn in *
+                    | LevelSetDecide.fsetdec ] ]
+       | [ H : List.In ?v ?ls |- LevelSet.In ?v' (List.fold_right ?f ?init (List.rev ?ls)) ]
+         => rewrite List.in_rev in H;
+            let ls' := fresh "ls" in
+            set (ls' := List.rev ls);
+            change (List.In v ls') in H;
+            change (LevelSet.In v' (List.fold_right f init ls'));
+            generalize init; induction ls'; cbn in *
+       end.
+  all: repeat first [ exfalso; assumption
+                    | progress destruct_head'_or
+                    | progress subst
+                    | progress intros
+                    | progress destruct ?
+                    | rewrite !LevelSetFact.add_iff
+                    | solve [ auto ] ].
+Qed.
+
+Definition consistent_dec ctrs : {@consistent ctrs} + {~@consistent ctrs}.
+Proof.
+  pose proof (@uGraph.is_consistent_spec config.default_checker_flags (levels_of_cs ctrs, ctrs) (levels_of_cs_spec ctrs)) as H.
+  destruct uGraph.is_consistent; [ left; apply H | right; intro H'; apply H in H' ]; auto.
+Defined.
+
+Definition levels_of_cs2 (cs1 cs2 : ConstraintSet.t) : LevelSet.t
+  := LevelSet.union (levels_of_cs cs1) (levels_of_cs cs2).
+Lemma levels_of_cs2_spec cs1 cs2 (lvls := levels_of_cs2 cs1 cs2)
+  : uGraph.global_uctx_invariants (lvls, cs1)
+    /\ uGraph.global_uctx_invariants (lvls, cs2).
+Proof.
+  split; apply global_uctx_invariants_union_or; constructor; apply levels_of_cs_spec.
+Qed.
+
+Definition levels_of_cscs (cs : ContextSet.t) (cstr : ConstraintSet.t) : LevelSet.t
+  := LevelSet.union (ContextSet.levels cs) (levels_of_cs2 cstr (ContextSet.constraints cs)).
+Lemma levels_of_cscs_spec cs cstr (lvls := levels_of_cscs cs cstr)
+  : uGraph.global_uctx_invariants (lvls, ContextSet.constraints cs)
+    /\ uGraph.global_uctx_invariants (lvls, cstr).
+Proof.
+  generalize (levels_of_cs2_spec cstr (ContextSet.constraints cs)).
+  split; apply global_uctx_invariants_union_or; constructor; apply levels_of_cs2_spec.
+Qed.
+
+Definition levels_of_algexpr (u : LevelAlgExpr.t) : VSet.t
+  := LevelExprSet.fold
+       (fun gc acc => match LevelExpr.get_noprop gc with
+                      | Some l => VSet.add l acc
+                      | None => acc
+                      end)
+       u
+       VSet.empty.
+Lemma levels_of_algexpr_spec u cstr (lvls := levels_of_algexpr u)
+  : gc_levels_declared (lvls, cstr) u.
+Proof.
+  subst lvls; cbv [levels_of_algexpr gc_levels_declared gc_expr_declared on_Some_or_None LevelExpr.get_noprop]; cbn [fst snd].
+  cbv [LevelExprSet.For_all]; cbn [fst snd].
+  repeat first [ apply conj
+               | progress intros
+               | progress destruct ?
+               | exact I
+               | progress rewrite <- ?LevelExprSet.elements_spec1, ?InA_In_eq in *
+               | rewrite LevelExprSetProp.fold_spec_right ].
+  all: lazymatch goal with
+       | [ H : List.In ?v ?ls |- VSet.In ?v' (List.fold_right ?f ?init (List.rev ?ls)) ]
+         => rewrite List.in_rev in H;
+            let ls' := fresh "ls" in
+            set (ls' := List.rev ls);
+            change (List.In v ls') in H;
+            change (VSet.In v' (List.fold_right f init ls'));
+            generalize init; induction ls'; cbn in *
+       end.
+  all: repeat first [ exfalso; assumption
+                    | progress destruct_head'_or
+                    | progress subst
+                    | progress intros
+                    | progress destruct ?
+                    | rewrite !VSetFact.add_iff
+                    | solve [ auto ] ].
+Qed.
+
+Definition leq0_levelalg_n_dec n ϕ u u' : {@leq0_levelalg_n (uGraph.Z_of_bool n) ϕ u u'} + {~@leq0_levelalg_n (uGraph.Z_of_bool n) ϕ u u'}.
+Proof.
+  pose proof (@uGraph.gc_leq0_levelalg_n_iff config.default_checker_flags (uGraph.Z_of_bool n) ϕ u u') as H.
+  pose proof (@uGraph.gc_consistent_iff config.default_checker_flags ϕ).
+  cbv [on_Some on_Some_or_None] in *.
+  destruct gc_of_constraints eqn:?.
+  all: try solve [ left; cbv [consistent] in *; hnf; intros; exfalso; intuition eauto ].
+  pose proof (fun G cstr => @uGraph.leqb_levelalg_n_spec G (LevelSet.union (levels_of_cs ϕ) (LevelSet.union (levels_of_algexpr u) (levels_of_algexpr u')), cstr)).
+  pose proof (fun x y => @gc_of_constraints_of_uctx config.default_checker_flags (x, y)) as H'.
+  pose proof (@is_consistent_spec config.default_checker_flags (levels_of_cs ϕ, ϕ)).
+  specialize_under_binders_by eapply gc_levels_declared_union_or.
+  specialize_under_binders_by eapply global_gc_uctx_invariants_union_or.
+  specialize_under_binders_by (constructor; eapply gc_of_uctx_invariants).
+  cbn [fst snd] in *.
+  specialize_under_binders_by eapply H'.
+  specialize_under_binders_by eassumption.
+  specialize_under_binders_by eapply levels_of_cs_spec.
+  specialize_under_binders_by reflexivity.
+  destruct is_consistent;
+    [ | left; now cbv [leq0_levelalg_n consistent] in *; intros; exfalso; intuition eauto ].
+  specialize_by intuition eauto.
+  let H := match goal with H : forall (b : bool), _ |- _ => H end in
+  specialize (H n u u').
+  specialize_under_binders_by (constructor; eapply gc_levels_declared_union_or; constructor; eapply levels_of_algexpr_spec).
+  match goal with H : is_true ?b <-> ?x, H' : ?y <-> ?x |- {?y} + {_} => destruct b eqn:?; [ left | right ] end.
+  all: intuition.
+Defined.
+
+Definition leq_levelalg_n_dec cf n ϕ u u' : {@leq_levelalg_n cf (uGraph.Z_of_bool n) ϕ u u'} + {~@leq_levelalg_n cf (uGraph.Z_of_bool n) ϕ u u'}.
+Proof.
+  cbv [leq_levelalg_n]; destruct (@leq0_levelalg_n_dec n ϕ u u'); destruct ?; auto.
+Defined.
+
+Definition eq0_levelalg_dec ϕ u u' : {@eq0_levelalg ϕ u u'} + {~@eq0_levelalg ϕ u u'}.
+Proof.
+  pose proof (@eq0_leq0_levelalg ϕ u u') as H.
+  destruct (@leq0_levelalg_n_dec false ϕ u u'), (@leq0_levelalg_n_dec false ϕ u' u); constructor; destruct H; split_and; now auto.
+Defined.
+
+Definition eq_levelalg_dec {cf ϕ} u u' : {@eq_levelalg cf ϕ u u'} + {~@eq_levelalg cf ϕ u u'}.
+Proof.
+  cbv [eq_levelalg]; destruct ?; auto using eq0_levelalg_dec.
+Defined.
+
+Definition eq_universe__dec {CS eq_levelalg ϕ}
+           (eq_levelalg_dec : forall u u', {@eq_levelalg ϕ u u'} + {~@eq_levelalg ϕ u u'})
+           s s'
+  : {@eq_universe_ CS eq_levelalg ϕ s s'} + {~@eq_universe_ CS eq_levelalg ϕ s s'}.
+Proof.
+  cbv [eq_universe_]; repeat destruct ?; auto.
+Defined.
+
+Definition eq_universe_dec {cf ϕ} s s' : {@eq_universe cf ϕ s s'} + {~@eq_universe cf ϕ s s'} := eq_universe__dec eq_levelalg_dec _ _.
+
+Definition valid_constraints_dec cf ϕ cstrs : {@valid_constraints cf ϕ cstrs} + {~@valid_constraints cf ϕ cstrs}.
+Proof.
+  pose proof (fun G a b c => uGraph.check_constraints_spec (uGraph.make_graph G) (levels_of_cs2 ϕ cstrs, ϕ) a b c cstrs) as H1.
+  pose proof (fun G a b c => uGraph.check_constraints_complete (uGraph.make_graph G) (levels_of_cs2 ϕ cstrs, ϕ) a b c cstrs) as H2.
+  pose proof (levels_of_cs2_spec ϕ cstrs).
+  cbn [fst snd] in *.
+  destruct (consistent_dec ϕ); [ | now left; cbv [valid_constraints valid_constraints0 consistent not] in *; destruct ?; intros; eauto; exfalso; eauto ].
+  destruct_head'_and.
+  specialize_under_binders_by assumption.
+  cbv [uGraph.is_graph_of_uctx MCOption.on_Some] in *.
+  cbv [valid_constraints] in *; repeat destruct ?; auto.
+  { specialize_under_binders_by reflexivity.
+    destruct uGraph.check_constraints_gen; specialize_by reflexivity; auto. }
+  { rewrite uGraph.gc_consistent_iff in *.
+    cbv [uGraph.gc_of_uctx monad_utils.bind monad_utils.ret monad_utils.option_monad MCOption.on_Some] in *; cbn [fst snd] in *.
+    destruct ?.
+    all: try congruence.
+    all: exfalso; assumption. }
+Defined.
+
+Definition valid_constraints0_dec ϕ ctrs : {@valid_constraints0 ϕ ctrs} + {~@valid_constraints0 ϕ ctrs}
+  := @valid_constraints_dec config.default_checker_flags ϕ ctrs.
+
+Definition is_lSet_dec cf ϕ s : {@is_lSet cf ϕ s} + {~@is_lSet cf ϕ s}.
+Proof.
+  apply eq_universe_dec.
+Defined.
+
+Definition is_allowed_elimination_dec cf ϕ allowed u : {@is_allowed_elimination cf ϕ allowed u} + {~@is_allowed_elimination cf ϕ allowed u}.
+Proof.
+  cbv [is_allowed_elimination is_true]; destruct ?; auto;
+    try solve [ repeat decide equality ].
+  destruct (@is_lSet_dec cf ϕ u), is_propositional; intuition auto.
+Defined.
diff --git a/common/theories/uGraph.v b/common/theories/uGraph.v
index 18074b8ce..e22b5a4a2 100644
--- a/common/theories/uGraph.v
+++ b/common/theories/uGraph.v
@@ -1429,7 +1429,7 @@ Section CheckLeq.
       gc_expr_declared e' ->
       leqb_expr_n_gen leqb_level_n_gen lt e e' ->
       gc_leq0_levelalg_n lt uctx.2 (LevelAlgExpr.make e) (LevelAlgExpr.make e').
-  Proof.
+  Proof using Type.
     unfold leqb_expr_n.
     destruct e as [l k], e' as [l' k'];
     try (cbn in *; discriminate);
@@ -1449,7 +1449,7 @@ Section CheckLeq.
       (HHl' : gc_expr_declared e')
     : leqb_expr_n_gen leqb_level_n_gen ⎩ n ⎭ e e'
       <-> gc_leq0_levelalg_n ⎩ n ⎭ uctx.2 (LevelAlgExpr.make e) (LevelAlgExpr.make e').
-  Proof.
+  Proof using HC.
     split; [apply (leqb_expr_n_spec0_gen _ leqb_correct)|]; try assumption.
     destruct e as [l k] eqn:eqe, e' as [l' k'] eqn:eqe'; cbn; intro H;
       destruct HC as [v0 Hv0]; pose proof (H v0 Hv0) as H0; cbn in H0.
@@ -1471,7 +1471,7 @@ Section CheckLeq.
     n e1 u
     : gc_expr_declared e1 -> gc_levels_declared u -> leqb_expr_univ_n_gen leqb_level_n_gen n e1 u
       -> gc_leq0_levelalg_n n uctx.2 (LevelAlgExpr.make e1) u.
-  Proof.
+  Proof using Type.
     unfold leqb_expr_univ_n_gen; intros He1 Hu H.
     unfold_univ_rel0.
     rewrite val_fold_right.
@@ -1565,7 +1565,7 @@ Section CheckLeq.
       gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 (LevelAlgExpr.make e) u ->
       exists (e' : LevelExpr.t), LevelExprSet.In e' u
             /\ gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 (LevelAlgExpr.make e) (LevelAlgExpr.make e').
-  Proof.
+  Proof using HC HG Huctx.
     intros Hl Hu H.
     assert (HG1 : invariants G) by (rewrite HG; exact _).
     assert (HG2 : acyclic_no_loop G) by (rewrite HG; exact _).
@@ -1855,7 +1855,7 @@ Section CheckLeq.
       (Hu  : gc_levels_declared u)
     : leqb_expr_univ_n_gen leqb_level_n_gen ⎩ lt ⎭ e1 u
       <-> gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 (LevelAlgExpr.make e1) u.
-  Proof.
+  Proof using HC HG Huctx.
     split; [eapply leqb_expr_univ_n_spec0_gen; eauto|].
     unfold leqb_expr_univ_n_gen; intro HH.
     case_eq (LevelAlgExpr.exprs u). intros e u' ee.
@@ -1889,7 +1889,7 @@ Section CheckLeq.
     (Hu1  : gc_levels_declared u1)
     (Hu2  : gc_levels_declared u2)
 : leqb_levelalg_n_gen leqb_level_n_gen lt u1 u2 -> gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 u1 u2.
-  Proof.
+  Proof using Type.
     unfold leqb_levelalg_n_gen. intros H.
     unfold_univ_rel0.
     unfold val, LevelAlgExpr.Evaluable.
@@ -1921,7 +1921,7 @@ Section CheckLeq.
         (Hu2  : gc_levels_declared l2)
     : leqb_levelalg_n_gen leqb_level_n_gen lt l1 l2
       <-> gc_leq0_levelalg_n ⎩ lt ⎭ uctx.2 l1 l2.
-  Proof.
+  Proof using HC HG Huctx.
     split; [eapply leqb_levelalg_n_spec0_gen; eauto |].
     unfold leqb_levelalg_n_gen; intro HH.
     unfold LevelAlgExpr.exprs.
@@ -1949,7 +1949,7 @@ Section CheckLeq.
      (Hu1  : gc_levels_declared u1)
      (Hu2  : gc_levels_declared u2)
     : check_leqb_levelalg_gen leqb_level_n_gen u1 u2 <-> gc_leq_levelalg uctx.2 u1 u2.
-  Proof.
+  Proof using HC HG Huctx.
     unfold check_leqb_levelalg_gen,
           gc_leq_levelalg, gc_leq_levelalg_n,
           leqb_levelalg_n_gen, gc_leq0_levelalg_n.
@@ -1975,7 +1975,7 @@ Section CheckLeq.
       (Hu1  : gc_levels_declared l1)
       (Hu2  : gc_levels_declared l2)
     : check_eqb_levelalg_gen leqb_level_n_gen l1 l2 <-> gc_eq_levelalg uctx.2 l1 l2.
-  Proof.
+  Proof using HC HG Huctx.
     unfold check_eqb_levelalg_gen, gc_eq_levelalg.
     destruct check_univs; [|split; trivial].
     split; cbn.
@@ -2024,7 +2024,7 @@ Section CheckLeq.
     (Hu1 : gc_levels_declared' uctx.1 gc)
     : check_gc_constraint_gen leqb_level_n_gen gc
       -> if check_univs then forall v, gc_satisfies v uctx.2 -> gc_satisfies0 v gc else True.
-  Proof.
+  Proof using Huctx.
     unfold check_gc_constraint_gen.
     destruct check_univs; [cbn|trivial].
     destruct gc as [l z l'|k l|k n|l k|n k].
@@ -2056,7 +2056,7 @@ Section CheckLeq.
     ctrs (Hu1 : gcs_levels_declared uctx.1 ctrs)
     : check_gc_constraints_gen leqb_level_n_gen ctrs
       -> if check_univs then forall v, gc_satisfies v uctx.2 -> gc_satisfies v ctrs else True.
-  Proof.
+  Proof using Huctx.
     rewrite /gcs_levels_declared in Hu1. pose proof check_gc_constraint_spec_gen as XX.
     unfold check_gc_constraints_gen. destruct check_univs; [cbn|trivial].
     intros HH v Hv.
@@ -3252,3 +3252,56 @@ Proof.
   unfold is_consistent. by move=> /on_SomeP [? [-> <-]].
 Qed.
 
+From MetaCoq.Utils Require Import MCUtils.
+
+Lemma global_uctx_invariants_union_or lvls1 lvls2 cs
+  : global_uctx_invariants (lvls1, cs) \/ global_uctx_invariants (lvls2, cs)
+    -> global_uctx_invariants (LevelSet.union lvls1 lvls2, cs).
+Proof.
+  cbv [global_uctx_invariants uctx_invariants ConstraintSet.For_all declared_cstr_levels]; cbn [fst snd ContextSet.levels ContextSet.constraints].
+  repeat first [ apply conj
+               | progress intros
+               | progress cbv beta iota in *
+               | progress destruct ?
+               | progress destruct_head'_and
+               | progress destruct_head'_or
+               | progress split_and
+               | rewrite !LevelSet.union_spec
+               | progress specialize_dep_under_binders_by eapply pair
+               | solve [ eauto ] ].
+Qed.
+
+Lemma global_gc_uctx_invariants_union_or lvls1 lvls2 cs
+  : global_gc_uctx_invariants (lvls1, cs) \/ global_gc_uctx_invariants (lvls2, cs)
+    -> global_gc_uctx_invariants (VSet.union lvls1 lvls2, cs).
+Proof.
+  cbv [global_gc_uctx_invariants uctx_invariants GoodConstraintSet.For_all declared_cstr_levels]; cbn [fst snd ContextSet.levels ContextSet.constraints].
+  repeat first [ apply conj
+               | progress intros
+               | progress cbv beta iota in *
+               | progress subst
+               | progress destruct ?
+               | progress destruct_head'_and
+               | progress destruct_head'_or
+               | progress split_and
+               | rewrite !VSet.union_spec
+               | progress specialize_dep_under_binders_by eassumption
+               | solve [ eauto ] ].
+Qed.
+
+Lemma gc_levels_declared_union_or lvls1 lvls2 cstr u
+  : gc_levels_declared (lvls1, cstr) u \/ gc_levels_declared (lvls2, cstr) u
+    -> gc_levels_declared (VSet.union lvls1 lvls2, cstr) u.
+Proof.
+  cbv [gc_levels_declared LevelExprSet.For_all gc_expr_declared on_Some_or_None LevelExpr.get_noprop]; cbn [fst].
+  repeat first [ apply conj
+               | progress intros
+               | progress cbv beta iota in *
+               | progress destruct ?
+               | progress destruct_head'_and
+               | progress destruct_head'_or
+               | progress split_and
+               | rewrite !VSet.union_spec
+               | progress specialize_dep_under_binders_by eassumption
+               | solve [ eauto ] ].
+Qed.