+lemma after_inv_true3: ∀cs1,cs2,tl. cs1 ⊚ cs2 ≡ Ⓣ @ tl →
+ ∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = Ⓣ @ tl2 & tl1 ⊚ tl2 ≡ tl.
+#cs1 #cs2 #tl #H elim (after_inv_inh3 … H) -H // *
+#tl1 #_ #H destruct
+qed-.
+
+lemma after_inv_false3: ∀cs1,cs2,tl. cs1 ⊚ cs2 ≡ Ⓕ @ tl →
+ (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = Ⓕ @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
+ ∃∃tl1. cs1 = Ⓕ @ tl1 & tl1 ⊚ cs2 ≡ tl.
+#cs1 #cs2 #tl #H elim (after_inv_inh3 … H) -H /2 width=1 by or_introl/ * /3 width=3 by ex2_intro, or_intror/
+qed-.
+