proposition: Theorem all_list_transmit : forall (P:nat->nat->Prop)(p:nat*nat)(l:list(nat*nat)), all_list P (p::l)-> all_list P l.
proof: Proof. intros P fst_elem l H l1 l2 p n Heq. unfold all_list in H. apply H with (fst_elem::l1) l2; rewrite Heq; auto. Qed.
imports: List Arith