proposition: Lemma ListEmpty_helper : forall {A} (seq: list A), (Nat.eqb (Datatypes.length seq) 0) = match seq with | nil => true | _ :: _ => false end.
proof: Proof. destruct seq; reflexivity. Qed.
imports: CertifiedExtraction.Extraction.External.Core Bedrock.Platform.Facade.examples.QsADTs