[GdT Log&Prog] [TT in Coq] TP