proposition: Lemma Vr_exten x y: cnfp x -> cnfp y -> (forall e, Vr x e = Vr y e) -> x = y.
proof: Proof. move: x y. suff H x y: cnfp x -> cnfp y -> (forall e, Vr x e = Vr y e) -> sub (range x) (range y). move => x y ox oy j; apply: (cnf_same_range ox oy). by apply: extensionality; apply H => //. move => ox oy h t /(range_gP (proj41 ox)) [i idx tv]. move: (Vr_correct ox idx); rewrite h => eq1. case: (inc_or_not (oexp x i) (domain (range y))) => ety. have ->: t = J (oexp x i)(ocoef x i) by rewrite tv ((proj43 ox) _ idx). rewrite - eq1 /Vr. apply: (fdomain_pr1 (cnf_range_fgraph oy) ety). move/cnfpP: ox => /proj43=> h1; case (proj2(proj2(proj33(h1 _ idx)))). by rewrite -/(ocoef x i)- eq1 /Vr (Vg_out_of_range ety). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)