+qed-.
+
+(* Properties with istot ****************************************************)
+
+lemma coafter_sor: ∀f. 𝐅❪f❫ → ∀f2. 𝐓❪f2❫ → ∀f1. f2 ~⊚ f1 ≘ f → ∀f1a,f1b. f1a ⋓ f1b ≘ f1 →
+ ∃∃fa,fb. f2 ~⊚ f1a ≘ fa & f2 ~⊚ f1b ≘ fb & fa ⋓ fb ≘ f.
+@isfin_ind
+[ #f #Hf #f2 #Hf2 #f1 #Hf #f1a #f1b #Hf1
+ lapply (coafter_fwd_isid2 … Hf ??) -Hf // #H2f1
+ elim (sor_inv_isid3 … Hf1) -Hf1 //
+ /3 width=5 by coafter_isid_dx, sor_idem, ex3_2_intro/
+| #f #_ #IH #f2 #Hf2 #f1 #H1 #f1a #f1b #H2
+ elim (coafter_inv_xxp … H1) -H1 [1,3: * |*: // ]
+ [ #g2 #g1 #Hf #Hgf2 #Hgf1
+ elim (sor_inv_xxp … H2) -H2 [ |*: // ] #ga #gb #Hg1
+ lapply (istot_inv_push … Hf2 … Hgf2) -Hf2 #Hg2
+ elim (IH … Hf … Hg1) // -f1 -g1 -IH -Hg2
+ /3 width=11 by coafter_refl, sor_pp, ex3_2_intro/
+ | #g2 #Hf #Hgf2
+ lapply (istot_inv_next … Hf2 … Hgf2) -Hf2 #Hg2
+ elim (IH … Hf … H2) // -f1 -IH -Hg2
+ /3 width=11 by coafter_next, sor_pp, ex3_2_intro/
+ ]
+| #f #_ #IH #f2 #Hf2 #f1 #H1 #f1a #f1b #H2
+ elim (coafter_inv_xxn … H1) -H1 [ |*: // ] #g2 #g1 #Hf #Hgf2 #Hgf1
+ lapply (istot_inv_push … Hf2 … Hgf2) -Hf2 #Hg2
+ elim (sor_inv_xxn … H2) -H2 [1,3,4: * |*: // ] #ga #gb #Hg1
+ elim (IH … Hf … Hg1) // -f1 -g1 -IH -Hg2
+ /3 width=11 by coafter_refl, coafter_push, sor_np, sor_pn, sor_nn, ex3_2_intro/
+]
+qed-.
+
+(* Properties with after ****************************************************)
+(*
+corec theorem coafter_trans1: ∀f0,f3,f4. f0 ~⊚ f3 ≘ f4 →
+ ∀f1,f2. f1 ~⊚ f2 ≘ f0 →
+ ∀f. f2 ~⊚ f3 ≘ f → f1 ~⊚ f ≘ f4.
+#f0 #f3 #f4 * -f0 -f3 -f4 #f0 #f3 #f4 #g0 [1,2: #g3 ] #g4
+[ #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
+ cases (coafter_inv_xxp … Hg0 … H0) -g0
+ #f1 #f2 #Hf0 #H1 #H2
+ cases (coafter_inv_ppx … Hg … H2 H3) -g2 -g3
+ #f #Hf #H /3 width=7 by coafter_refl/
+| #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
+ cases (coafter_inv_xxp … Hg0 … H0) -g0
+ #f1 #f2 #Hf0 #H1 #H2
+ cases (coafter_inv_pnx … Hg … H2 H3) -g2 -g3
+ #f #Hf #H /3 width=7 by coafter_push/
+| #Hf4 #H0 #H4 #g1 #g2 #Hg0 #g #Hg
+ cases (coafter_inv_xxn … Hg0 … H0) -g0 *
+ [ #f1 #f2 #Hf0 #H1 #H2
+ cases (coafter_inv_nxx … Hg … H2) -g2
+ #f #Hf #H /3 width=7 by coafter_push/
+ | #f1 #Hf0 #H1 /3 width=6 by coafter_next/
+ ]
+]
+qed-.
+
+corec theorem coafter_trans2: ∀f1,f0,f4. f1 ~⊚ f0 ≘ f4 →
+ ∀f2, f3. f2 ~⊚ f3 ≘ f0 →
+ ∀f. f1 ~⊚ f2 ≘ f → f ~⊚ f3 ≘ f4.
+#f1 #f0 #f4 * -f1 -f0 -f4 #f1 #f0 #f4 #g1 [1,2: #g0 ] #g4
+[ #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
+ cases (coafter_inv_xxp … Hg0 … H0) -g0
+ #f2 #f3 #Hf0 #H2 #H3
+ cases (coafter_inv_ppx … Hg … H1 H2) -g1 -g2
+ #f #Hf #H /3 width=7 by coafter_refl/
+| #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
+ cases (coafter_inv_xxn … Hg0 … H0) -g0 *
+ [ #f2 #f3 #Hf0 #H2 #H3
+ cases (coafter_inv_ppx … Hg … H1 H2) -g1 -g2
+ #f #Hf #H /3 width=7 by coafter_push/
+ | #f2 #Hf0 #H2
+ cases (coafter_inv_pnx … Hg … H1 H2) -g1 -g2
+ #f #Hf #H /3 width=6 by coafter_next/
+ ]
+| #Hf4 #H1 #H4 #f2 #f3 #Hf0 #g #Hg
+ cases (coafter_inv_nxx … Hg … H1) -g1
+ #f #Hg #H /3 width=6 by coafter_next/
+]
+qed-.
+*)