proposition: Theorem EqLTrans : forall L : list A, transitive (list A) EqL.
proof: Proof. intros L; red in |- *. intros x y z H'; generalize z; Elimc H'; clear z; auto. intros a b L1 L2 H' H'0 H'1 z H'2; inversion H'2; auto. apply EqLCons; auto. apply eqATrans with (y := b); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)