Typeable3 Formula  
Bijection (Combination (Formula v p f)) (Combination (Formula v p f))  
(Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Predicate p, Function f v, Variable v, Constants (Predicate p (PTerm v f)), FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v) => Eq (Formula v p f)  
(Typeable (Formula v p f), Data v, Data p, Data f) => Data (Formula v p f)  
(Eq (Formula v p f), Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Predicate p, Function f v, Variable v) => Ord (Formula v p f)  Here are the magic Ord and Eq instances

(Show v, Show p, Show f) => Show (Formula v p f)  
(SafeCopy v0, SafeCopy p0, SafeCopy f0) => SafeCopy (Formula v0 p0 f0)  
Negatable (Formula v p f)  
(Predicate p, Function f v) => HasFixity (Formula v p f)  
(Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Pretty v, Show v, Variable v, Pretty p, Show p, Predicate p, Pretty f, Show f, Function f v) => Pretty (Formula v p f)  
(Negatable (Formula v p f), Formula (Formula v p f) (Predicate p (PTerm v f)), Constants (Formula v p f), Constants (Formula v p f), Variable v, Predicate p, Function f v) => Combinable (Formula v p f)  
(Constants (Formula v p f), Predicate p, Variable v, Function f v) => Constants (Formula v p f)  
(Predicate p, Function f v) => Formula (Formula v p f) (Predicate p (PTerm v f))  
(Ord (Formula v p f), Negatable (Formula v p f), Combinable (Formula v p f), Constants (Formula v p f), Pretty (Formula v p f), Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Show v, Show p, Show f, HasFixity (Formula v p f), Variable v, Predicate p, Function f v) => PropositionalFormula (Formula v p f) (Predicate p (PTerm v f))  
(Combinable (Formula v p f), Constants (Formula v p f), Constants (Predicate p (PTerm v f)), HasFixity (Predicate p (PTerm v f)), Pretty (Predicate p (PTerm v f)), Pretty v, Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v  
Bijection (Formula v p f) (Formula v p f)  