pr0/fwd pr0_gen_void
pr0/dec nf0_dec
-pr0/subst1 pr0_subst1_back
-pr0/subst1 pr0_subst1_fwd
-pr1/pr1 pr1_strip
-pr1/pr1 pr1_confluence
-pr1/props pr1_pr0
-pr1/props pr1_t
-pr1/props pr1_head_1
-pr1/props pr1_head_2
-pr1/props pr1_comp
+
pr1/props pr1_eta
+
pr2/fwd pr2_gen_void
pr3/fwd pr3_gen_void
-pr3/pr1 pr3_pr1
pr3/props pr3_eta
sn3/props sns3_lifts
sty1/cnt sty1_cnt
-sty1/props sty1_trans
-sty1/props sty1_bind
-sty1/props sty1_appl
-sty1/props sty1_lift
-sty1/props sty1_correct
-sty1/props sty1_abbr
-sty1/props sty1_cast2
subst/fwd subst_sort
subst/fwd subst_lref_lt
subst/fwd subst_lref_eq
ty3/arity_props ty3_predicative
ty3/arity_props ty3_repellent
ty3/arity_props ty3_acyclic
-ty3/arity_props ty3_sn3
ty3/dec ty3_inference
-ty3/fwd ty3_gen_appl
ty3/fwd tys3_gen_nil
ty3/fwd tys3_gen_cons
ty3/fwd_nf2 ty3_gen_appl_nf2