(* Basic inversions ********************************************************)
+lemma ppc_inv_empty:
+ (š) Ļµ š ā ā„.
+#H0 @H0 -H0 //
+qed-.
+
lemma ppc_inv_lcons (p):
p Ļµ š ā āāl,q. lāq = p.
*
-[ #H elim H -H //
+[ #H0 elim (ppc_inv_empty ā¦ H0)
| #l #q #_ /2 width=3 by ex1_2_intro/
]
qed-.