-val empty_subst : substitution
-val apply_subst : substitution -> Cic.term -> Cic.term
-val apply_subst_metasenv : substitution -> Cic.metasenv -> Cic.metasenv
-val ppsubst : substitution -> string
-val buildsubst :
- int -> Cic.context -> Cic.term -> Cic.term -> substitution ->
- substitution
-val flatten_subst : substitution -> substitution
-val lookup_subst : Cic.term -> substitution -> Cic.term
-val filter : substitution -> Cic.metasenv -> Cic.metasenv
-val is_in_subst : int -> substitution -> bool
-val merge_subst_if_possible:
- substitution -> substitution ->
- substitution option