proposition: Lemma propToWord_list_empty_map: forall A B (lst : list A) (x : W) (f : A -> B), Programming.propToWord (map f lst = nil) x -> Programming.propToWord (lst = nil) x.
proof: Proof. intros. unfold Programming.propToWord, IF_then_else in *. setoid_rewrite (map_eq_nil_iff f lst) in H; assumption. Qed.
imports: CertifiedExtraction.Extraction.External.Core Bedrock.Platform.Facade.examples.QsADTs