proposition: Lemma expr_sound {d c f g h} : termD d c f = Some h → f ≈ g → exprD (Equiv d c f g).
proof: Proof. intros. simple apply exprAD_sound'. specialize (X d c). revert X. unfold expr_tauto. destruct (expr_backward _); intuition. simple eapply exprSD_enough; eauto. Qed.
imports: Equations(Equations) Category.Lib Category.Lib.IList Category.Theory.Category Category.Solver.Expr Category.Solver.Denote Category.Solver.Reify Category.Solver.Normal