proposition: Theorem interCom : forall L1 L2 L3 L4 : list A, inter L1 L2 L3 -> inter L2 L1 L4 -> Olist L1 -> Olist L2 -> Olist L3 -> Olist L4 -> EqL L3 L4.
proof: Proof. intros L1 L2 L3 L4 H' H'0 H'1 H'2 H'3 H'4. apply EqLOlist; auto. apply interMin with (L1 := L2) (L2 := L1); auto. apply interIncl2 with (L1 := L1); auto. apply interIncl1 with (L2 := L2); auto. apply interMin with (L1 := L1) (L2 := L2); auto. apply interIncl2 with (L1 := L2); auto. apply interIncl1 with (L2 := L1); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)