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