proposition: Lemma L1' (a: T1) : T1omega * (a * T1omega) = T1omega * a * T1omega.
proof: Proof. by rewrite mulA. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0) Coq(Relations Basics Wellfounded.Inverse_Image Wellfounded.Inclusion)