proposition: Theorem interfCom : forall L1 L2 : list A, Olist L1 -> Olist L2 -> EqL (interf L1 L2) (interf L2 L1).
proof: Proof. intros L1 L2 H' H'0. apply interCom with (L1 := L1) (L2 := L2); auto. apply interfOlist; auto. apply interfOlist; auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)