+#S #A #w %
+ [* #l generalize in match w; -w cases l [normalize #w * /2/]
+ #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
+ #w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl))
+ % /2/ whd @(ex_intro … tl) /2/
+ |* [2: normalize #eqw <eqw @(ex_intro … (nil ?)) /2/]
+ (* caso interessante *)
+ cut (∀w1,w2.w=w1@w2 → cat S A A^* w2 → A^* w2)
+ [2:#H @(H … (nil ?)) //]
+ elim w
+ [#w1 #w2 #H cases (nil_to_nil … (sym_eq … H)) #_ #H >H #_
+ @(ex_intro … (nil ?)) /2/
+ |#a #w1 #Hind *
+ [#w2 whd in ⊢ ((???%)→?); #eqw2 <eqw2 *
+ #w3 * #w4 cases w3
+ [* * whd in ⊢ ((??%?)→?); #H <H //
+ |#b #w5 * * whd in ⊢ ((??%?)→?); #H destruct
+ #H1 * #l * #H2 #H3 @(ex_intro … ((a::w5)::l)) %
+ normalize // /2/
+ ]
+ |#b #w2 #w3 whd in ⊢ ((???%)→?); #H destruct #H1
+ @(Hind … w2) //
+ ]
+ ]
+ ]
+qed.
+
+axiom star_epsilon: ∀S:DeqSet.∀A:word S → Prop.