proposition: Lemma CompileTupleListEmpty_alt_helper {A}: forall lst w, Programming.propToWord (lst = @nil A) w -> ret (bool2w match lst with | nil => true | _ :: _ => false end) ↝ w.
proof: Proof. intros * h. apply CompileEmpty_helper in h. rewrite <- ListEmpty_helper. assumption. Qed.
imports: CertifiedExtraction.Extraction.External.Core Bedrock.Platform.Facade.examples.QsADTs