proposition: Lemma dynE (A B : Type) interp (v : interp A) (w : interp B) : jmeq interp v w <-> dyn interp v = dyn interp w.
proof: Proof. by split=>[[pf ->]|[pf]]; subst B; [rewrite !eqc | move/dyn_inj=>->]. Qed.
imports: Coq(ssreflect ssrfun Eqdep ClassicalFacts) pcm(options)