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