proposition: Lemma Exercise6_12d n f: natp n -> Ex6_12_ax f n -> Ex6_12_v f n = Yo (n = \0c) \1o ((f \1c) *o oprodf (fun i => (osucc (omega0 *o (Yo (csucc i = n) \1o (f (csucc (csucc i))))))) n).
proof: Proof. move => nN pa. rewrite /Ex6_12_v /CNFpv {1 2} /Ex6_12_ec /Ex6_12_e /Ex6_12_c. aw; Ytac0; Ytac0. case (equal_or_not n \0c) => nz; aw;repeat Ytac0. by rewrite nz /CNFpv1 oprod_f0 oopow0 !(oprod1l OS1). rewrite oopow0 (oprod1l (OS_nat (proj1(pa _ (proj1 (Exercise6_12a nN nz)))))). apply: f_equal. apply:(oprodf_exten nN) => i [_ lin]. rewrite /Ex6_12_ec /Ex6_12_e /Ex6_12_c /CNFp_value1/cantor_pmon. by aw; rewrite /CNFp_value1 !(Y_false lin) oopow1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)