proposition: Theorem from_morphism_to_morphism {d c} {t : Term} {f} : termD d c (from_morphism (to_morphism t)) = Some f → termD d c t ≈ Some f.
proof: Proof. generalize dependent c. generalize dependent d. unfold termD; induction t; simpl; intros; desh. - pose proof (from_morphism_app Heqo); desh. specialize (IHt2 _ _ x1). rewrite e in IHt2; clear e. specialize (IHt1 _ _ x0). rewrite x3 in IHt1; clear x3. rewrite EqDec.peq_dec_refl in IHt1, IHt2. specialize (IHt1 eq_refl). specialize (IHt2 eq_refl). simpl in *; desh. rewrite Heqo1, EqDec.peq_dec_refl. now rewrite IHt1, IHt2, <- x2. Qed.
imports: Coq.Lists.List Equations(Equations) Category.Lib Category.Theory.Category Category.Solver.Expr Category.Solver.Denote Category.Solver.Reify