+
+(* 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-.