proposition: Lemma from_morphism_app_r {d m c} {t1 t2 : Morphism} {g h} : termD_work m (from_morphism t1) = Some (c; g) → termD_work d (from_morphism t2) = Some (m; h) → ∃ f, f ≈ g ∘ h ∧ termD_work d (from_morphism (combine t1 t2)) = Some (c; f).
proof: Proof. generalize dependent c. generalize dependent d. generalize dependent t2. unfold termD; destruct t1; simpl; intros; desh. generalize dependent c0. induction c; simpl; intros; desh. - destruct t2; simpl in *; desh. exists (g ∘ h). split; cat. now rewrite H1, H0. - destruct t2; simpl in *; desh. + specialize (IHc _ _ eq_refl); desh. exists (h1 ∘ x0). split. * now rewrite x1; cat. * now rewrite e0, Heqo0. + specialize (IHc _ _ eq_refl); desh. exists (h1 ∘ x0). split. * now rewrite x1; cat. * now rewrite e0, Heqo0. Qed.
imports: Coq.Lists.List Equations(Equations) Category.Lib Category.Theory.Category Category.Solver.Expr Category.Solver.Denote Category.Solver.Reify