+lemma in_comp_iref (t) (q) (k):
+ q ϵ t → 𝗱k◗𝗺◗q ϵ 𝛕k.t.
+/2 width=3 by ex2_intro/ qed.
+
+(* Basic inversions *********************************************************)
+
+lemma in_comp_inv_iref (t) (p) (k):
+ p ϵ 𝛕k.t →
+ ∃∃q. 𝗱k◗𝗺◗q = p & q ϵ t.
+#t #p #k * #q #Hq #Hp
+/2 width=3 by ex2_intro/
+qed-.
+
+(* COMMENT