proposition: Lemma CompileCallFacadeImplementationOfConstructor: forall `{FacadeWrapper av A} {env} (adt: A) tenv, forall fpointer, GLabelMap.MapsTo fpointer (Axiomatic (FacadeImplementationOfConstructor _ adt)) env -> forall vret ext, vret ∉ ext -> NotInTelescope vret tenv -> {{ tenv }} (Call vret fpointer nil) {{ [[ `vret ->> adt as _]] :: tenv }} ∪ {{ ext }} // env.
proof: Proof. repeat match goal with | _ => SameValues_Facade_t_step | _ => facade_cleanup_call | _ => PreconditionSet_t end. facade_eauto. facade_eauto. Qed.
imports: Coq.Lists.List CertifiedExtraction.Extraction.External.Core