proposition: Theorem exprSD_enough {d c f g h} : termD d c f = Some h → exprSD (Equiv d c f g) → exprAD (Equiv d c f g).
proof: Proof. simpl; intros. rewrite H1. apply from_morphism_to_morphism_r in H0. rewrite H1 in H0. destruct (termD _ _ _) eqn:?. + reflexivity. + tauto. Qed.
imports: Coq.Lists.List Equations(Equations) Category.Lib Category.Theory.Category Category.Solver.Expr Category.Solver.Denote Category.Solver.Reify