+
+(* Advanced inversions ******************************************************)
+
+lemma in_comp_inv_abst_hd (t) (p):
+ (šāp) Ļµ š.t ā p Ļµ t.
+#t #p #H0
+elim (in_comp_inv_abst ā¦ H0) -H0 #q #H0 #Hq
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
+qed-.
+
+lemma in_comp_inv_appl_sd (u) (t) (p):
+ (š¦āp) Ļµ ļ¼ u.t ā p Ļµ u.
+#u #t #p #H0
+elim (in_comp_inv_appl ā¦ H0) -H0 * #q #H0 #Hq
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
+qed-.
+
+lemma in_comp_inv_appl_hd (u) (t) (p):
+ (šāp) Ļµ ļ¼ u.t ā p Ļµ t.
+#u #t #p #H0
+elim (in_comp_inv_appl ā¦ H0) -H0 * #q #H0 #Hq
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
+qed-.