/2 width=1 by exteq_repl/ qed-.
(* Constructions with compose ***********************************************)
lemma compose_repl_fwd_dx (A) (B) (C) (g) (f1) (f2):
/2 width=1 by exteq_repl/ qed-.
(* Constructions with compose ***********************************************)
lemma compose_repl_fwd_dx (A) (B) (C) (g) (f1) (f2):