proposition: Theorem EqLOlist : forall L1 L2 : list A, Olist L1 -> Olist L2 -> InclEq L1 L2 -> InclEq L2 L1 -> EqL L1 L2.
proof: Proof. intros L1; elim L1; auto. intros L2; case L2; auto. intros a l H' H'0 H'1 H'2; inversion H'2. lapply (H a); [ intros H'4; inversion H'4 | idtac ]; auto. intros a l H' L2; case L2; auto. intros H'0 H'1 H'2; inversion H'2. lapply (H a); [ intros H'4; inversion H'4 | idtac ]; auto. intros a0 l0 H'0 H'1 H'2 H'3; auto. apply EqLCons; auto. 2: apply H'; auto. 2: apply OlistInv with (a := a); auto. 2: apply OlistInv with (a := a0); auto. 2: apply InclEqOlist with (a := a) (b := a0); auto. 2: apply InclEqOlist with (a := a0) (b := a); auto. inversion H'3. lapply (H a0); [ intros H'5; inversion H'5 | idtac ]; auto. inversion H'2; auto. lapply (H6 a); [ intros H'6; inversion H'6 | idtac ]; auto. absurd (ltA a0 a); auto. apply ltAntiSym; auto. apply OlistSupEq with (L := l); auto. apply OlistSupEq with (L := l0); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)