proposition: Lemma CompileCallAny: forall {av} (env : GLabelMap.t (FuncSpec av)), forall fpointer tenv, GLabelMap.MapsTo fpointer (Axiomatic FAny) env -> forall var ext, var ∉ ext -> NotInTelescope var tenv -> {{ tenv }} (DFacade.Call var fpointer nil) {{ [[ ` var ~~> Any as _]] :: tenv }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call); facade_eauto. Qed.
imports: CertifiedExtraction.Extraction.Extraction