Data.Logic.Resolution

prove

getSetOfSupport

type SetOfSupport lit v term

type Unification lit v term

isRenameOfAtomEq

getSubstAtomEq