-(* Basic inversion lemmas on after ******************************************)
-
-fact after_inv_O1_aux: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g1. f1 = 0@g1 →
- (∃∃g2,g. g1 ⊚ g2 ≡ g & f2 = 0@g2 & f = 0@g) ∨
- ∃∃g2,g,b2,b. g1 ⊚ b2@g2 ≡ b@g & f2 = ⫯b2@g2 & f = ⫯b@g.
-#f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #b1
-[ #b2 #b #Ht #H1 #H2 #H3 #g1 #H destruct /3 width=5 by ex3_2_intro, or_introl/
-| #b2 #b #a2 #a #Ht #H1 #H2 #H3 #g1 #H destruct /3 width=7 by ex3_4_intro, or_intror/
-| #b #a1 #a #_ #H1 #H3 #g1 #H destruct
-]
-qed-.
-
-fact after_inv_O1_aux2: ∀f1,f2,f,b1,b2,b. b1@f1 ⊚ b2@f2 ≡ b@f → b1 = 0 →
- (∧∧ f1 ⊚ f2 ≡ f & b2 = 0 & b = 0) ∨
- ∃∃a2,a. f1 ⊚ a2@f2 ≡ a@f & b2 = ⫯a2 & b = ⫯a.
-#f1 #f2 #f #b1 #b2 #b #Ht #H elim (after_inv_O1_aux … Ht) -Ht [4: // |2: skip ] *
-[ #g2 #g #Hu #H1 #H2 destruct /3 width=1 by and3_intro, or_introl/
-| #g2 #g #a2 #a #Hu #H1 #H2 destruct /3 width=5 by ex3_2_intro, or_intror/
-]
-qed-.
-
-lemma after_inv_O1: ∀g1,f2,f. 0@g1 ⊚ f2 ≡ f →
- (∃∃g2,g. g1 ⊚ g2 ≡ g & f2 = 0@g2 & f = 0@g) ∨
- ∃∃g2,g,b2,b. g1 ⊚ b2@g2 ≡ b@g & f2 = ⫯b2@g2 & f = ⫯b@g.
-/2 width=3 by after_inv_O1_aux/ qed-.
-
-fact after_inv_zero_aux2: ∀f1,f2,f,b1,b2,b. b1@f1 ⊚ b2@f2 ≡ b@f → b1 = 0 → b2 = 0 →
- f1 ⊚ f2 ≡ f ∧ b = 0.
-#f1 #f2 #f #b1 #b2 #b #Ht #H1 #H2 elim (after_inv_O1_aux2 … Ht H1) -Ht -H1 *
-[ /2 width=1 by conj/
-| #a1 #a2 #_ #H0 destruct
-]
-qed-.
-
-lemma after_inv_zero: ∀g1,g2,f. 0@g1 ⊚ 0@g2 ≡ f →
- ∃∃g. g1 ⊚ g2 ≡ g & f = 0@g.
-#g1 #g2 #f #H elim (after_inv_O1 … H) -H *
-[ #x2 #g #Hu #H1 #H2 destruct /2 width=3 by ex2_intro/
-| #x2 #g #a2 #a #Hu #H destruct
-]
-qed-.
-
-fact after_inv_skip_aux2: ∀f1,f2,f,b1,b2,b. b1@f1 ⊚ b2@f2 ≡ b@f → b1 = 0 → ∀a2. b2 = ⫯a2 →
- ∃∃a. f1 ⊚ a2@f2 ≡ a@f & b = ⫯a.
-#f1 #f2 #f #b1 #b2 #b #Ht #H1 #a2 #H2 elim (after_inv_O1_aux2 … Ht H1) -Ht -H1 *
-[ #_ #H0 destruct
-| #x2 #x #H #H0 #H1 destruct /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma after_inv_skip: ∀g1,g2,f,b2. 0@g1 ⊚ ⫯b2@g2 ≡ f →
- ∃∃g,b. g1 ⊚ b2@g2 ≡ b@g & f = ⫯b@g.
-#g1 #g2 * #b #f #b2 #Ht elim (after_inv_skip_aux2 … Ht) [2,4: // |3: skip ] -Ht
-#a #Ht #H destruct /2 width=4 by ex2_2_intro/
-qed-.
-
-fact after_inv_S1_aux: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g1,b1. f1 = ⫯b1@g1 →
- ∃∃g,b. b1@g1 ⊚ f2 ≡ b@g & f = ⫯b@g.
-#f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #b1
-[ #b2 #b #_ #H1 #H2 #H3 #g1 #a1 #H destruct
-| #b2 #b #a2 #a #_ #H1 #H2 #H3 #g1 #a1 #H destruct
-| #b #a1 #a #Ht #H1 #H3 #g1 #x1 #H destruct /2 width=4 by ex2_2_intro/
-]
-qed-.
-
-fact after_inv_S1_aux2: ∀f1,f2,f,b1,b. b1@f1 ⊚ f2 ≡ b@f → ∀a1. b1 = ⫯a1 →
- ∃∃a. a1@f1 ⊚ f2 ≡ a@f & b = ⫯a.
-#f1 #f2 #f #b1 #b #Ht #a #H elim (after_inv_S1_aux … Ht) -Ht [4: // |2,3: skip ]
-#g #x #Hu #H0 destruct /2 width=3 by ex2_intro/
-qed-.
-
-lemma after_inv_S1: ∀g1,f2,f,b1. ⫯b1@g1 ⊚ f2 ≡ f →
- ∃∃g,b. b1@g1 ⊚ f2 ≡ b@g & f = ⫯b@g.
-/2 width=3 by after_inv_S1_aux/ qed-.
-
-fact after_inv_drop_aux2: ∀f1,f2,f,a1,a. a1@f1 ⊚ f2 ≡ a@f → ∀b1,b. a1 = ⫯b1 → a = ⫯b →
- b1@f1 ⊚ f2 ≡ b@f.
-#f1 #f2 #f #a1 #a #Ht #b1 #b #H1 #H elim (after_inv_S1_aux2 … Ht … H1) -a1
-#x #Ht #Hx destruct //
-qed-.
-
-lemma after_inv_drop: ∀f1,f2,f,b1,b. ⫯b1@f1 ⊚ f2 ≡ ⫯b@f → b1@f1 ⊚ f2 ≡ b@f.
-/2 width=5 by after_inv_drop_aux2/ qed-.
-
-fact after_inv_O3_aux1: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g. f = 0@g →
- ∃∃g1,g2. g1 ⊚ g2 ≡ g & f1 = 0@g1 & f2 = 0@g2.
-#f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #b1
-[ #b2 #b #Ht #H1 #H2 #H3 #g #H destruct /2 width=5 by ex3_2_intro/
-| #b2 #b #a2 #a #_ #H1 #H2 #H3 #g #H destruct
-| #b #a1 #a #_ #H1 #H3 #g #H destruct
-]
-qed-.
-
-fact after_inv_O3_aux2: ∀f1,f2,f,b1,b2,b. b1@f1 ⊚ b2@f2 ≡ b@f → b = 0 →
- ∧∧ f1 ⊚ f2 ≡ f & b1 = 0 & b2 = 0.
-#f1 #f2 #f #b1 #b2 #b #Ht #H1 elim (after_inv_O3_aux1 … Ht) [2: // |3: skip ] -b
-#g1 #g2 #Ht #H1 #H2 destruct /2 width=1 by and3_intro/
-qed-.
-
-lemma after_inv_O3: ∀f1,f2,g. f1 ⊚ f2 ≡ 0@g →
- ∃∃g1,g2. g1 ⊚ g2 ≡ g & f1 = 0@g1 & f2 = 0@g2.
-/2 width=3 by after_inv_O3_aux1/ qed-.
-
-fact after_inv_S3_aux1: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g,b. f = ⫯b@g →
- (∃∃g1,g2,b2. g1 ⊚ b2@g2 ≡ b@g & f1 = 0@g1 & f2 = ⫯b2@g2) ∨
- ∃∃g1,b1. b1@g1 ⊚ f2 ≡ b@g & f1 = ⫯b1@g1.
-#f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #b1
-[ #b2 #b #_ #H1 #H2 #H3 #g #a #H destruct
-| #b2 #b #a2 #a #HT #H1 #H2 #H3 #g #x #H destruct /3 width=6 by ex3_3_intro, or_introl/
-| #b #a1 #a #HT #H1 #H3 #g #x #H destruct /3 width=4 by ex2_2_intro, or_intror/
-]
-qed-.
-
-fact after_inv_S3_aux2: ∀f1,f2,f,a1,a2,a. a1@f1 ⊚ a2@f2 ≡ a@f → ∀b. a = ⫯b →
- (∃∃b2. f1 ⊚ b2@f2 ≡ b@f & a1 = 0 & a2 = ⫯b2) ∨
- ∃∃b1. b1@f1 ⊚ a2@f2 ≡ b@f & a1 = ⫯b1.
-#f1 #f2 #f #a1 #a2 #a #Ht #b #H elim (after_inv_S3_aux1 … Ht) [3: // |4,5: skip ] -a *
-[ #g1 #g2 #b2 #Ht #H1 #H2 destruct /3 width=3 by ex3_intro, or_introl/
-| #g1 #b1 #Ht #H1 destruct /3 width=3 by ex2_intro, or_intror/
-]
-qed-.
-
-lemma after_inv_S3: ∀f1,f2,g,b. f1 ⊚ f2 ≡ ⫯b@g →
- (∃∃g1,g2,b2. g1 ⊚ b2@g2 ≡ b@g & f1 = 0@g1 & f2 = ⫯b2@g2) ∨
- ∃∃g1,b1. b1@g1 ⊚ f2 ≡ b@g & f1 = ⫯b1@g1.
-/2 width=3 by after_inv_S3_aux1/ qed-.
-
-(* Advanced inversion lemmas on after ***************************************)
-
-fact after_inv_O2_aux2: ∀f1,f2,f,a1,a2,a. a1@f1 ⊚ a2@f2 ≡ a@f → a2 = 0 →
- a1 = a ∧ f1 ⊚ f2 ≡ f.
-#f1 #f2 #f #a1 #a2 elim a1 -a1
-[ #a #H #H2 elim (after_inv_zero_aux2 … H … H2) -a2 /2 width=1 by conj/
-| #a1 #IH #a #H #H2 elim (after_inv_S1_aux2 … H) -H [3: // |2: skip ]
- #b #H #H1 elim (IH … H) // -a2
- #H2 destruct /2 width=1 by conj/
-]
-qed-.
-
-lemma after_inv_O2: ∀f1,g2,f. f1 ⊚ 0@g2 ≡ f →
- ∃∃g1,g,a. f1 = a@g1 & f = a@g & g1 ⊚ g2 ≡ g.
-* #a1 #f1 #f2 * #a #f #H elim (after_inv_O2_aux2 … H) -H //
-/2 width=6 by ex3_3_intro/
-qed-.