proposition: Lemma CompileRead': forall {A} `{FacadeWrapper (Value av) A} (vfrom vto : string) (a: A) (tenv tenv0: Telescope av) ext env, vto ∉ ext -> vfrom <> vto -> NotInTelescope vto tenv0 -> (forall a, is_adt (wrap a) = false) -> TelEq ext tenv ([[` vfrom ->> a as _]] :: tenv0) -> {{ tenv }} Assign vto (Var vfrom) {{ [[ ` vto ->> a as _]]::tenv }} ∪ {{ ext }} // env.
proof: Proof. intros * ? ? ? ? H; setoid_rewrite H. destruct (not_adt_is_sca H4). SameValues_Facade_t. f_equal; auto. match goal with | [ H: wrap _ = wrap _ |- _ ] => rewrite H end; SameValues_Facade_t. 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