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