kdrag.GFP

kdrag.GFP(F, sort=None)

>>> ZSet = smt.SetSort(smt.IntSort())
>>> F = smt.Array("F", ZSet, ZSet)
>>> GFP(F)
Lambda(x!...,
    Exists(A!...,
            And(subset(A!..., F[A!...]), A!...[x!...])))