Prog_Prove.Types_and_funs