-(* Basic inversion lemmas on after ******************************************)
-
-fact after_inv_OOx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. g1 = ↑f1 → g2 = ↑f2 →
- ∃∃f. f1 ⊚ f2 ≡ f & g = ↑f.
-#g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
-[ #g2 #g #Hf #H1 #H2 #H #x1 #x2 #Hx1 #Hx2 destruct
- <(injective_push … Hx1) <(injective_push … Hx2) -x2 -x1
- /2 width=3 by ex2_intro/
-| #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
- elim (discr_next_push … Hx2)
-| #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
- elim (discr_next_push … Hx1)
-]
-qed-.
-
-lemma after_inv_OOx: ∀f1,f2,g. ↑f1 ⊚ ↑f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ↑f.
-/2 width=5 by after_inv_OOx_aux/ qed-.
-
-fact after_inv_OSx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. g1 = ↑f1 → g2 = ⫯f2 →
- ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
-#g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
-[ #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
- elim (discr_push_next … Hx2)
-| #g2 #g #Hf #H1 #H2 #H3 #x1 #x2 #Hx1 #Hx2 destruct
- <(injective_push … Hx1) <(injective_next … Hx2) -x2 -x1
- /2 width=3 by ex2_intro/
-| #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
- elim (discr_next_push … Hx1)
-]
-qed-.
-
-lemma after_inv_OSx: ∀f1,f2,g. ↑f1 ⊚ ⫯f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
-/2 width=5 by after_inv_OSx_aux/ qed-.
-
-fact after_inv_Sxx_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g → ∀f1. g1 = ⫯f1 →
- ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
-#g1 #f2 #g * -g1 -f2 -g #f1 #f2 #f #g1
-[ #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
- elim (discr_push_next … Hx1)
-| #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
- elim (discr_push_next … Hx1)
-| #g #Hf #H1 #H #x1 #Hx1 destruct
- <(injective_next … Hx1) -x1
- /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma after_inv_Sxx: ∀f1,f2,g. ⫯f1 ⊚ f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
-/2 width=5 by after_inv_Sxx_aux/ qed-.
-
-(* Advanced inversion lemmas on after ***************************************)
-
-fact after_inv_OOO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
- ∀f1,f2,f. g1 = ↑f1 → g2 = ↑f2 → g = ↑f → f1 ⊚ f2 ≡ f.
-#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
-#x #Hf #Hx destruct >(injective_push … Hx) -f //
-qed-.
-
-fact after_inv_OOS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
- ∀f1,f2,f. g1 = ↑f1 → g2 = ↑f2 → g = ⫯f → ⊥.
-#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
-#x #Hf #Hx destruct elim (discr_next_push … Hx)
-qed-.
-
-fact after_inv_OSS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
- ∀f1,f2,f. g1 = ↑f1 → g2 = ⫯f2 → g = ⫯f → f1 ⊚ f2 ≡ f.
-#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2
-#x #Hf #Hx destruct >(injective_next … Hx) -f //
-qed-.
-
-fact after_inv_OSO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
- ∀f1,f2,f. g1 = ↑f1 → g2 = ⫯f2 → g = ↑f → ⊥.
-#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2
-#x #Hf #Hx destruct elim (discr_push_next … Hx)
-qed-.
-
-fact after_inv_SxS_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g →
- ∀f1,f. g1 = ⫯f1 → g = ⫯f → f1 ⊚ f2 ≡ f.
-#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_Sxx_aux … Hg … H1) -g1
-#x #Hf #Hx destruct >(injective_next … Hx) -f //
-qed-.
-
-fact after_inv_SxO_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g →
- ∀f1,f. g1 = ⫯f1 → g = ↑f → ⊥.
-#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_Sxx_aux … Hg … H1) -g1
-#x #Hf #Hx destruct elim (discr_push_next … Hx)
-qed-.
-
-fact after_inv_OxO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
- ∀f1,f. g1 = ↑f1 → g = ↑f →
- ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ↑f2.
-#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H
-[ elim (after_inv_OSO_aux … Hg … H1 … H) -g1 -g -f1 -f //
-| lapply (after_inv_OOO_aux … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma after_inv_OxO: ∀f1,g2,f. ↑f1 ⊚ g2 ≡ ↑f →
- ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ↑f2.
-/2 width=5 by after_inv_OxO_aux/ qed-.
-
-fact after_inv_OxS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
- ∀f1,f. g1 = ↑f1 → g = ⫯f →
- ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ⫯f2.
-#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H
-[ lapply (after_inv_OSS_aux … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/
-| elim (after_inv_OOS_aux … Hg … H1 … H) -g1 -g -f1 -f //
-]
-qed-.
-
-fact after_inv_xxO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. g = ↑f →
- ∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ↑f2.
-* * [2: #m1 ] #g1 #g2 #g #Hg #f #H
-[ elim (after_inv_SxO_aux … Hg … H) -g2 -g -f //
-| elim (after_inv_OxO_aux … Hg … H) -g /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma after_inv_xxO: ∀g1,g2,f. g1 ⊚ g2 ≡ ↑f →
- ∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ↑f2.
-/2 width=3 by after_inv_xxO_aux/ qed-.
-
-fact after_inv_xxS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. g = ⫯f →
- (∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ⫯f2) ∨
- ∃∃f1. f1 ⊚ g2 ≡ f & g1 = ⫯f1.
-* * [2: #m1 ] #g1 #g2 #g #Hg #f #H
-[ /4 width=5 by after_inv_SxS_aux, or_intror, ex2_intro/
-| elim (after_inv_OxS_aux … Hg … H) -g
- /3 width=5 by or_introl, ex3_2_intro/
-]
-qed-.
-
-lemma after_inv_xxS: ∀g1,g2,f. g1 ⊚ g2 ≡ ⫯f →
- (∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ⫯f2) ∨
- ∃∃f1. f1 ⊚ g2 ≡ f & g1 = ⫯f1.
-/2 width=3 by after_inv_xxS_aux/ qed-.