proposition: Lemma CNFB_unique X1 X2: CNFB_ax X1 -> CNFB_ax X2 -> CNFBv X1 = CNFBv X2 -> X1 = X2.
proof: Proof. move => [p1 p2 p3 p4] [q1 q2 q3 q4] sv. move:(CNFb_unique p2 q2 p4 q4 sv) =>[sa sb]. apply: (fgraph_exten p1 q1 sa) => i idx. move/(NltP p2): (idx) => /sb [e1 e2]. rewrite - (p3 _ idx). by rewrite sa in idx; rewrite - (q3 _ idx) -/(oexp _ _) -/(ocoef _ _)e1 e2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)