fact: Fixpoint collect_annot (k: kind) (f : GFormula k) : list AA := match f with | TT _ | FF _ | X _ => nil | A _ _ a => a ::nil | AND f1 f2 | OR f1 f2 | IFF f1 f2 | EQ f1 f2 | IMPL f1 _ f2 => collect_annot f1 ++ collect_annot f2 | NOT f => collect_annot f end.
imports: List Refl Bool Relation_Definitions Setoid