+[|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
+qed-.
+
+(* Advanced destructions ****************************************************)
+
+lemma pcc_des_d_dx (o) (p) (n) (k):
+ pโ๐ฑk ฯต ๐โจo,nโฉ โ p ฯต ๐โจo,n+kโฉ.
+#o #p #n #k #H0
+elim (pcc_inv_d_dx โฆ H0) -H0 #H1 #H2 //
+qed-.
+
+lemma pcc_des_gen (o) (p) (n):
+ p ฯต ๐โจo,nโฉ โ p ฯต ๐โจโป,nโฉ.
+#o #p #n #H0 elim H0 -p -n //
+#p #n [ #k #Ho ] #_ #IH
+/2 width=1 by pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx, pcc_false_d_dx/