proposition: Lemma sublist_forall : forall {A: Type} (P : A -> Prop) l1 l2, Forall P l2 -> sublist l1 l2 -> Forall P l1.
proof: Proof. intros. induction H0. constructor. inv H. tauto. inv H. constructor; auto. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List