proposition: Corollary exprAD_sound' {cat} (env : Arrows cat) (e : Expr) : exprAD e → exprD e.
proof: Proof. apply exprAD_sound. Qed.
imports: Coq.Lists.List Equations(Equations) Category.Lib Category.Theory.Category Category.Solver.Expr Category.Solver.Denote Category.Solver.Reify