proposition: Lemma proper_trace_cpring : proper_trace (behead et).
proof: Proof. have:= memc0_trace_cpring; rewrite trace_cpring_eq !inE -(eq_sym e2). by case/norP=> _ /norP[]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)