fact: Fixpoint exprD (e : Expr) : Type := match e with | Top => True | Bottom => False | And p q => exprD p ∧ exprD q | Or p q => exprD p + exprD q | Impl p q => exprD p → exprD q | Equiv d c f g => match termD d c f, termD d c g with | Some f, Some g => f ≈ g | _, _ => False end end.
imports: Equations(Equations) Category.Lib Category.Lib.IList Category.Theory.Category Category.Solver.Expr