proposition: Theorem EqLInv : forall (L1 L2 : list A) (a : A), EqL L1 L2 -> InEq a L1 -> InEq a L2.
proof: Proof. intros L1 L2 a H'; elim H'; auto. intros a0 b L3 L4 H'0 H'1 H'2 H'3; inversion H'3; auto. apply InEqHead; auto. apply eqATrans with (y := a0); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)