+(* Basic constructions *******************************************************)
+
+lemma in_comp_iref (t) (q) (k):
+ q ϵ t → 𝗱k◗𝗺◗q ϵ 𝛕k.t.
+/2 width=3 by ex2_intro/ qed.
+
+lemma in_comp_iref2 (t) (q) (k) (d):
+ q ϵ t → 𝗱❨k,d❩◗𝗺◗q ϵ 𝛕❨k,d❩.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-.
+
+lemma in_comp_inv_iref2 (t) (p) (k) (d):
+ p ϵ 𝛕❨k,d❩.t →
+ ∃∃q. 𝗱❨k,d❩◗𝗺◗q = p & q ϵ t.
+#t #p #k #d * #q #Hq #Hp
+/2 width=3 by ex2_intro/
+qed-.