proposition: Theorem all_list_add : forall (P:nat->nat->Prop)(l:list(nat*nat))(p n:nat), P p n -> all_list P l -> all_list P ((p,n)::l).
proof: Proof. intros P l p n Hp Hal l1; case l1. intros l2 p' n' Heq; injection Heq; intros Hl Hn' Hp'; rewrite <- Hn'; rewrite <- Hp'; auto. simpl; clear l1; intros fst_elem l1 l2 p' n' Heq; injection Heq; intros Hl Hfst; apply (Hal l1 l2); assumption. Qed.
imports: List Arith