proposition: Lemma CNFb_exten e1 c1 e2 c2 n: same_below e1 e2 n -> same_below c1 c2 n -> CNFb_ax e1 c1 n -> natp n -> (CNFb_ax e2 c2 n /\ CNFbv e1 c1 n = CNFbv e2 c2 n).
proof: Proof. move => h1 h2 [ax1 ax2] nN. move: (CNFq_exten h1 h2 ax1 nN) => [ax3 ->]; split => //; split => //. by move => i lin; rewrite - (h2 _ lin);apply: ax2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)