proposition: Lemma Forall_rew : forall {T: Type} [P: T -> Prop] (l : list T), Forall P l <-> match l with | nil => True | e::l => P e /\ Forall P l end.
proof: Proof. destruct l. - split ; auto. - split ; intro. inv H. tauto. destruct H. constructor ; auto. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List