-(* telescopic non-delifting substitution of l in M.
- * [this is the telescoping delifting substitution lifted by |l|]
+theorem subst_app: ∀M,N,k,L. (App M N)[k≝L] = App M[k≝L] N[k≝L].
+// qed.
+
+theorem subst_lambda: ∀N,M,k,L. (Lambda N M)[k≝L] = Lambda N[k≝L] M[k+1≝L].
+// qed.
+
+theorem subst_prod: ∀N,M,k,L. (Prod N M)[k≝L] = Prod N[k≝L] M[k+1≝L].
+// qed.
+
+(* telescopic delifting substitution of l in M.