proposition: Lemma formula_ex0_pr (x := formula_ex0) X: nonempty X -> [/\ formulap x, formula_len x = \2c, free_vars x = emptyset & (formula_val X x) = \0c].
proof: Proof. move => [w wX]. rewrite /x /formula_ex0. set a := (J val_eq (J \0c \0c)). set b := (J val_ex (J \0c a)). set c := (J val_not b). have v0: variablep \0c by apply:NS0. move:(free_vars_eq v0 v0); rewrite -/a -/(singleton _) => fva. case: (fkind_eq_p2 v0 v0); rewrite -/a => fa fla. move:(fkind_ex_p2 v0 fa); rewrite -/b fla succ_zero; move =>[fb flb]. move: (free_vars_ex v0 fa); rewrite -/b fva setC_v => fvb. move:(fkind_not_p2 fb); rewrite -/fb -/c flb succ_one;move =>[fc flc]. move:(free_vars_not fb); rewrite -/fc -/c fvb => fvd. split => //. set Va:= (formula_val X a). set Vb:= (formula_val X b). set Vc := formula_val X c. move:(proj33 (formula_val_eq X v0 v0)); rewrite -/a -/Va;move => Vap. move: (proj33 (formula_val_ex X v0 fa)); rewrite -/b -/Vb fvb => Vbp. move: (proj33(formula_val_not X fb)); rewrite -/Vc -/Vb -/c => Vcp. case: (emptyset_dichot Vc) => // [][ f /Vcp [/gfunctions_P2 [ga gb gc]]]; case. move: gb; rewrite fvd => /domain_set0_P ->; apply /Vbp; split. apply/gfunctions_P2; split; aw; fprops; apply: fgraph_set0. set g := Lg (singleton \0c) (fun z => w). exists g. move : (set1_1 \0c) => zz. rewrite /g;apply /Vap; rewrite LgV// Lgd; split;fprops. by rewrite /restr /Lg funI_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)