-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/
+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/