proposition: Lemma fkind_in_p1 x (b:= (P (Q x))) (c := Q (Q x)): formulap x -> P x = val_in -> [/\ x = J val_in (J b c), variablep b & variablep c].
proof: Proof. move => pa pb. have pc: (P x = val_in \/ P x = val_eq) by left. move/(fkind_pa pa): pc => /atomic_formulaP [qa qb qc qd qe]; split => //. by rewrite - pb qb qa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)