proposition: Lemma not_adt_is_sca : forall {A} `{FacadeWrapper (Value av) A}, (forall (a: A), is_adt (wrap a) = false) -> exists w, (forall a, wrap a = SCA _ (w a)).
proof: Proof. intros. exists (fun a => match wrap a with SCA x => x | _ => Word.wzero 32 end). intros; specialize (H0 a); destruct (wrap a); unfold is_adt in *; congruence. Qed.
imports: Fiat.CertifiedExtraction.Extraction.Extraction Fiat.CertifiedExtraction.Extraction.BinEncoders.Basics Fiat.CertifiedExtraction.Extraction.BinEncoders.Wrappers Fiat.CertifiedExtraction.Extraction.BinEncoders.Properties Coq.Program.Program Coq.Lists.List