proposition: Lemma emptyRaster_wf : forall n m, raster_well_formed (emptyRaster n m).
proof: Proof. split. - apply repeat_length. - apply Forall_forall. intros. apply repeat_spec in H. subst x. apply repeat_length. Qed.
imports: CoRN.stdlib_omissions.List Coq.Arith.Arith Coq.PArith.BinPos