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