fact: Definition Lifted_is_true {av} ext tenv test := @LiftPropertyToTelescope av ext (fun st => is_true st test) tenv.
imports: Coq.Classes.Morphisms CertifiedExtraction.Core CertifiedExtraction.Utils Coq.Setoids.Setoid