\ /
V_______________________________________________________________ *)
-include "lambda/lift.ma".
-
+include "pts_dummy/lift.ma".
+(*
let rec subst t k a ≝
match t with
[ Sort n ⇒ Sort n
(A [i ≝ B]) [i+k ≝ C] = (A [i+k+1 := C]) [i ≝ B [k ≝ C]].
#A #B #C #k #i >commutative_plus >subst_lemma //
qed.
+*)