proposition: Lemma jm_trans A B C (u : interp A) (v : interp B) (w : interp C) : jmeq u v -> jmeq v w -> jmeq u w.
proof: Proof. by case=>? -> [? ->]; subst B C; rewrite !eqc; apply: jm_refl. Qed.
imports: Coq(ssreflect ssrfun Eqdep ClassicalFacts) pcm(options)