Indfun_common Glob_termops Recdef Glob_term_to_relation Functional_principles_proofs Functional_principles_types Invfun Indfun Merge G_indfun