proposition: Lemma CNFq_ax_exten e1 c1 e2 c2 n: same_below e1 e2 n -> same_below c1 c2 n -> CNFq_ax e1 c1 n -> CNFq_ax e2 c2 n.
proof: Proof. move => h1 h2 [a1 a2 a3 a4]; split => //. + by move => i lin; rewrite - (h1 _ lin);apply: a2. + by move => i lin; rewrite - (h2 _ lin);apply: a3. + move => i iN lin; rewrite - (h1 _ lin). by rewrite -(h1 _ (cle_ltT (cleS iN) lin)); apply:a4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)