proposition: Lemma map_eq_nil_iff {A B} (f: A -> B): forall l, map f l = nil <-> l = nil.
proof: Proof. destruct l; simpl; split; reflexivity || discriminate. Qed.
imports: CertifiedExtraction.Extraction.External.Core Bedrock.Platform.Facade.examples.QsADTs