proposition: Lemma CompileEmpty_helper {A}: forall (lst : list A) (w : W), Programming.propToWord (lst = @nil A) w -> ret (bool2w (Nat.eqb (Datatypes.length lst) 0)) ↝ w.
proof: Proof. unfold Programming.propToWord, IF_then_else in *. destruct lst; simpl in *; destruct 1; repeat cleanup; try discriminate; fiat_t. Qed.
imports: CertifiedExtraction.Extraction.External.Core Bedrock.Platform.Facade.examples.QsADTs