proposition: Theorem length_list_prod: forall (A : Set) (l1 l2 : list A), length (list_prod l1 l2) = length l1 * length l2.
proof: Proof. intros A l1 l2; elim l1; simpl; auto. intros a l H; rewrite length_app; rewrite length_map; rewrite H; auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat