proposition: Lemma formula_ext3 a X (z := J (J val_eq (J \0c \1c))(singleton (J \1c a))): inc a X -> (LS_setU X z = singleton a /\ forall Y, inc a Y -> (inc z (LS_nextP_aux Y X))).
proof: Proof. move => aX; rewrite /z; clear z. set phi :=J val_eq (J \0c \1c). move: (simple_fct NS1 aX); set f := (singleton (J \1c a)). move => [fgf df rf sd1 [sd2 fv1]]. set phi0 := J phi f. have v0: variablep \0c by apply: NS0. have v1: variablep \1c by apply: NS1. move:(free_vars_eq v0 v1); rewrite -/phi => fvphi. case: (fkind_eq_p2 v0 v1); rewrite -/phi => fa _. move: (proj33(formula_val_eq X v0 v1)); rewrite -/phi => Ha. have fphi0: pformula phi0. rewrite /phi0 /pformula;split; aww. rewrite df fvphi => t /set1_P ->; fprops. have fvphi0:pfree_vars phi0 = singleton \0c. rewrite /pfree_vars /phi0 pr1_pair pr2_pair fvphi df. apply: set1_pr; first by apply/setC1_P; split; fprops. by move => z /setC_P [/set2_P h /set1_P z1]; case: h. have h1: (singletonp (pfree_vars phi0)) by rewrite fvphi0; exists \0c. set phi' := (J val_ex (J \0c phi)). move:(pformula_inst_p1 fphi0 h1). rewrite /pformula_inst fvphi0 setU_1 /phi0; aw. rewrite -/phi; move => [q1 q2 q3 q4]. have r1: pformula_in X (J phi f) by split => //; aw. have fv3: free_vars (P phi0) = doubleton \0c \1c by rewrite /phi0; aw. have fv2: domain (Q phi0) = singleton \1c by rewrite /phi0; aw. have va: (doubleton \0c \1c -s1 \1c) = singleton \0c. set_extens t; first by move => /setC1_P [/set2_P]; case => // -> _;fprops. move /set1_P => ->; apply /setC1_P; split; fprops. have vd: domain f +s1 \0c = doubleton \0c \1c. rewrite df; set_extens t. case/setU1_P; [ move /set1_P => ->; fprops | move => ->; fprops ]. case /set2_P => ->; apply /setU1_P; [by right | by left; fprops ]. have vb:(singleton \1c +s1 union (singleton \0c)) = doubleton \0c \1c. by rewrite setU_1 - df. have vc: (union (pfree_vars phi0)) = \0c. by rewrite /pfree_vars /phi0; aw; rewrite fvphi df va setU_1. have sa: ~ inc \0c (domain f) by rewrite df => /set1_P; fprops. have sb: inc \1c (domain f) by rewrite df; fprops. have r2: inc a (LS_setU X phi0). apply /Zo_P; split => //; apply/ pfree_vars_closed_pr. rewrite /pclosed /pfree_vars; aw; rewrite fv3 domain_setU1 fv2 va vb. by rewrite setC_v. aw; rewrite vc; rewrite /phi0; aw. move: (formula_val_eq X v0 v1) => []; rewrite -/phi => _ Hb Hc. apply /Hc; rewrite setU1_V_out // setU1_V_in // domain_setU1 vd. by split => //; apply: fgraph_setU1. have r3: LS_setU X (J phi f) = singleton a. apply set1_pr => // z /(LS_setU_P _ r1 h1); aw. rewrite fvphi0 setU_1; move => [zx sc sd se]. move /(pfree_vars_closed_pr X sd): se; aw; move /Ha => [_ _ Hb _]. by move: Hb; rewrite setU1_V_out // setU1_V_in // fv1. split => //. move => Y aY; apply /Zo_P. have r4: sub (range f) X by rewrite /f range_set1 => t /set1_P ->. have r4': sub (range f) Y by rewrite /f range_set1 => t /set1_P ->. have r5: inc (J phi f) (pformulas_in X). by apply/pformulas_inP;split=> //; aw. have r6: domain f = free_vars (J val_ex (J \0c phi)). rewrite (free_vars_ex v0 fa) df fvphi //; set_extens t. move => /set1_P ->; apply /setC1_P; fprops. move => /setC1_P [/set2_P]; case => // -> _; fprops. have r7: inc f (formula_values Y (J val_ex (J \0c phi))). apply /gfunctions_P2; split => //. split => //; split => //. rewrite /pformula_inst fvphi0 setU_1; aw. apply /(pfree_vars_closed_pr _ q2); aw. move:(formula_val_ex Y v0 fa) => [_ sc sd]; apply/sd; split => //. move :(restr_setU1 a fgf sa); set g := _ +s1 _ => r8. exists g; last by rewrite - r6 r8. move: (proj33(formula_val_eq Y v0 v1)); rewrite -/phi => Hb; apply /Hb. rewrite /g domain_setU1 setU1_V_out // setU1_V_in // fv1 vd; split => //. by apply: fgraph_setU1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)