proposition: Lemma contVT B (P : B -> B -> Prop) : (forall x x', B = B -> x =jm x' -> P x x') <-> forall x, P x x.
proof: Proof. split; first by move=>H x; exact: (H x x (erefl _) (jmeq_refl _)). by move=>H x x' _; move/jmE=>->. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq) Eqdep ClassicalFacts