\ /
V_______________________________________________________________ *)
-include "lambda/subst.ma".
-include "basics/list.ma".
-
+include "pts_dummy/subst.ma".
+include "basics/lists/list.ma".
+(*
(*************************** substl *****************************)
let rec substl (G:list T) (N:T) : list T ≝
#P #G #v #w #Hv #t #u #Ht
lapply (substitution_tj … Ht ? ([]) … Hv) normalize //
qed.
+*)