fact: Fixpoint epsilon_pred a (e: expr_ops (ord Pred) BL) := match e with | e_bot => false | e_top => true | e_var i => a i | e_cup e f => epsilon_pred a e ||| epsilon_pred a f | e_cap e f => epsilon_pred a e &&& epsilon_pred a f | e_neg e => negb (epsilon_pred a e) end.
imports: kat lsyntax positives sups glang comparisons boolean