proposition: Lemma formula_ex1_pr (x := formula_ex1) X: [/\ formulap x, formula_len x = \3c, free_vars x = emptyset & (formula_val X x) = \1c].
proof: Proof. rewrite /x /formula_ex1. set a := (J val_eq (J \0c \0c)). set b := (J val_not a). set c := (J val_ex (J \0c b)). set d := (J val_not c). 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_not_p2 fa); rewrite -/fa -/b fla succ_zero;move =>[fb flb]. move:(free_vars_not fa); rewrite -/fb -/b fva => fvb. move:(fkind_ex_p2 v0 fb); rewrite -/c flb succ_one; move =>[fc flc]. move: (free_vars_ex v0 fb); rewrite -/c fvb setC_v => fvc. move:(fkind_not_p2 fc); rewrite -/fc -/d flc -/card_three;move =>[fd fld]. move:(free_vars_not fc); rewrite -/fd -/d fvc => fvd. split => //. set Va:= (formula_val X a). set Vb:= (formula_val X b). set Vc := formula_val X c. set Vd := formula_val X d. move:(proj33 (formula_val_eq X v0 v0)); rewrite -/a -/Va;move => Vap. move: (proj33(formula_val_not X fa)); rewrite -/Vb -/Va -/b => Vbp. move: (proj33 (formula_val_ex X v0 fb)); rewrite -/c -/Vc fvc => Vcp. move: (proj33(formula_val_not X fc)); rewrite -/Vd -/Vc -/d => Vdp. have eq1: (formula_values X d) = \1c. by rewrite /formula_values fvd gfunctions_empty. have qa:inc emptyset (formula_values X d) by rewrite eq1; apply /set1_P. apply: set1_pr; last by move => z /Vdp; rewrite eq1; move => [/set1_P]. apply/Vdp; split => // /Vcp [_ [g /Vbp [ ga gb] _]]; case: gb; apply/Vap. move/gfunctions_P2: ga; rewrite fvb; move => [gb gc gd]; split => //. apply: gd; apply /(range_gP gb); exists \0c => //; rewrite gc; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)