(* Basic constructions ******************************************************)
lemma ppc_lcons (l) (q): lāq Ļµ š.
-#l #p #H destruct
+#l #q #H0 destruct
+qed.
+
+lemma ppc_rcons (l) (q): qāl Ļµ š.
+#l #q #H
+elim (eq_inv_list_empty_rcons ??? H)
qed.
(* Basic inversions ********************************************************)
| #l #q #_ /2 width=3 by ex1_2_intro/
]
qed-.
+
+lemma ppc_inv_rcons (p):
+ p Ļµ š ā āāq,l. qāl = p.
+#p @(list_ind_rcons ā¦ p) -p
+[ #H0 elim (ppc_inv_empty ā¦ H0)
+| #q #l #_ #_ /2 width=3 by ex1_2_intro/
+]
+qed-.