proposition: Lemma next_formulasP F x : inc x (next_formulas F) <-> [\/ (inc x F), [/\ pairp x, P x = val_not & inc (Q x) F ], [/\ pairp x, P x = val_or, pairp (Q x), inc (P (Q x)) F & inc (Q (Q x)) F] | [/\ pairp x, P x = val_ex, pairp (Q x), variablep (P (Q x)) & inc (Q (Q x)) F] ].
proof: Proof. split. case/setU2_P; last first. by move/setX_P => [px /set1_P pa /setX_P[pb pc pd]]; constructor 4. case/setU2_P; last first. by move/setX_P => [pa /set1_P pb /setX_P[pc pd pe]]; constructor 3. case/setU2_P; first by constructor 1. by move/setX_P => [pa /set1_P pb pc]; constructor 2. case. + move => h; apply /setU2_P; left; apply /setU2_P; left; fprops. + move => [pa pb pc]; apply /setU2_P; left; apply /setU2_P; left. apply/setU2_P; right; apply /setX_P; split => //; rewrite pb; fprops. + move => [pa pb pc pd pe]; apply /setU2_P; left; apply/setU2_P; right. apply /setX_P; split => //; [rewrite pb; fprops | by apply /setX_P]. + move => [pa pb pc pd pe]; apply /setU2_P; right; apply /setX_P; split => //. rewrite pb; fprops. by apply /setX_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)