proposition: Lemma atomic_formulaP x: atomic_formulap x <-> [/\ pairp x, pairp (Q x), variablep (P (Q x)), variablep (Q (Q x)) & (P x = val_in \/ P x = val_eq)].
proof: Proof. split. move => /setX_P [px /set2_P pa /setX_P[pc pd pe] ]; split => //. by move => [pa pb pc pd /set2_P pe]; apply/setX_P; split => //; apply/setX_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)