(* This file was automatically generated: do not edit *********************)
-include "lift/defs.ma".
+include "LambdaDelta-1/lift/defs.ma".
inductive subst0: nat \to (T \to (T \to (T \to Prop))) \def
| subst0_lref: \forall (v: T).(\forall (i: nat).(subst0 i v (TLRef i) (lift