fact: Definition relate (p : pos_atom) (q : pos_atom) (qpos : bool) : atom_relation := if qpos then relate' p q else match relate' p q with | ARimply => ARcontradict | ARcontradict => ARimply | ARunknown => ARunknown end.
imports: Reals List Bool Gappa_common