fact: Record state : Set := {glob_ctx : env; glob_names : prt_names; glob_wf_ctx : wf glob_ctx; glob_length : length glob_ctx = length glob_names; glob_unique : name_unique glob_names}.
imports: Termes Conv Types Conv_Dec Infer Expr