lemma cpcs_repl (h) (G) (L): replace_2 … (cpcs h G L) (cpcs h G L) (cpcs h G L).
/3 width=5 by cpcs_trans, cpcs_sym/ qed-.
(*
lemma cpcs_repl (h) (G) (L): replace_2 … (cpcs h G L) (cpcs h G L) (cpcs h G L).
/3 width=5 by cpcs_trans, cpcs_sym/ qed-.
(*