fact: Fixpoint PreconditionSet_helper {av} (tenv: Telescope av) (ext: StringMap.t (Value av)) (vars: list string) := match vars with | nil => True | cons var vars => (not (StringMap.In var ext)) /\ NotInTelescope var tenv /\ PreconditionSet_helper tenv ext vars end.
imports: CertifiedExtraction.Core CertifiedExtraction.PropertiesOfTelescopes