proposition: Theorem interfProp1 : forall L1 L2 : list A, inter L1 L2 (interf L1 L2).
proof: Proof. intros L1; elim L1; simpl in |- *. intros L2; case L2; simpl in |- *; intros; apply interNil2; auto. intros a l H' L2; case L2; simpl in |- *; auto with datatypes core. apply interNil1; auto. intros a0 l0. case (ltADec a a0); intros s; [ Casec s; intros s | idtac ]. apply interLtA1; auto. apply interLtA2; auto. elim l0; auto. apply interNil1; auto. intros a1 l1 H'0. case (ltADec a a1); intros s1; [ Casec s1; intros s1 | idtac ]. apply interLtA1; auto. apply interLtA2; auto. apply interEqA; auto. apply interEqA; auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)