proposition: Theorem exprAD_sound (e : Expr) : exprAD e ↔ exprD e.
proof: Proof. induction e; split; simpl in *; intuition. - destruct (termD _ _ _) eqn:?; [|tauto]. destruct (termD _ _ (_ (_ g))) eqn:?; [|tauto]. apply from_morphism_to_morphism in Heqo. apply from_morphism_to_morphism in Heqo0. simpl in *. destruct (termD _ _ f); [|tauto]. destruct (termD _ _ g); [|tauto]. now rewrite Heqo, Heqo0, <- X. - desh. destruct (termD _ _ f) eqn:?; [|tauto]. destruct (termD _ _ g) eqn:?; [|tauto]. apply from_morphism_to_morphism_r in Heqo. apply from_morphism_to_morphism_r in Heqo0. simpl in *. destruct (termD _ _ _) eqn:?; [|tauto]. destruct (termD _ _ (_ (_ g))) eqn:?; [|tauto]. now rewrite Heqo, Heqo0, X. Qed.
imports: Coq.Lists.List Equations(Equations) Category.Lib Category.Theory.Category Category.Solver.Expr Category.Solver.Denote Category.Solver.Reify