proposition: Lemma sc_trans i j k : sub_ctx i j -> sub_ctx j k -> sub_ctx i k.
proof: Proof. by case=>K1 V1 [K2 V2]; split; [move: K2 | move: V2]; apply: prefix_trans. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)