pr1/props pr1_comp
pr1/props pr1_eta
pr2/clen pr2_gen_ctail
-pr2/subst1 pr2_gen_cabbr
-
-# check ######################################################################
-
pr2/fwd pr2_gen_void
pr2/props pr2_ctail
-
-# waiting ####################################################################
-
+pr2/subst1 pr2_gen_cabbr
pr3/fwd pr3_gen_sort
pr3/fwd pr3_gen_abst
pr3/fwd pr3_gen_cast
sty1/props sty1_correct
sty1/props sty1_abbr
sty1/props sty1_cast2
-subst0/dec dnf_dec2
-subst0/dec dnf_dec
-subst1/props subst1_ex
subst/fwd subst_sort
subst/fwd subst_lref_lt
subst/fwd subst_lref_eq
subst/fwd subst_head
subst/props subst_lift_SO
subst/props subst_subst0
-T/dec terms_props__bind_dec
-T/dec bind_dec_not
-T/dec terms_props__flat_dec
-T/dec terms_props__kind_dec
-T/dec term_dec
T/dec binder_dec
T/dec abst_dec
tlist/props tslt_wf__q_ind
tlist/props theads_tapp
tlist/props tcons_tapp_ex
tlist/props tlist_ind_rev
-T/props not_abbr_abst
-T/props not_void_abst
-T/props not_abbr_void
-T/props not_abst_void
-T/props thead_x_y_y
-T/props tweight_lt
ty3/arity ty3_arity
ty3/arity_props ty3_predicative
ty3/arity_props ty3_repellent
wf3/ty3 wf3_pr3_conf
wf3/ty3 wf3_pc3_conf
wf3/ty3 wf3_ty3_conf
+
+# check ######################################################################