include "delayed_updating/substitution/lift_prototerm.ma".
(* LIFT FOR PROTOTERM *******************************************************)
include "delayed_updating/substitution/lift_prototerm.ma".
(* LIFT FOR PROTOTERM *******************************************************)