proposition: Lemma WrapInstance_wrap : forall `{H: FacadeWrapper av A} (x: A), wrap x = ADT (wrap x).
proof: Proof. destruct H; intros; reflexivity. Qed.
imports: CertifiedExtraction.PureUtils CertifiedExtraction.Core Bedrock.Memory