(* Constructions with prototerm constructors ********************************)
-lemma ppc_iref (t) (n):
- (šn.t) Ļµ š.
-#t #n #p * #q #Hq #H0 destruct //
+lemma ppc_iref (t) (k):
+ (šk.t) Ļµ š.
+#t #k #p * #q #Hq #H0 destruct //
+qed.
+
+lemma ppc_iref2 (t) (k) (d):
+ (šāØk,dā©.t) Ļµ š.
+#t #k #d #p * #q #Hq #H0 destruct //
qed.