proposition: Lemma fkind_eq_p2 a b (x := J val_eq (J a b)): variablep a -> variablep b -> (formulap x /\ formula_len x = \0c).
proof: Proof. move => pb pc. have pd: atomic_formulap x. rewrite /x;apply/atomic_formulaP; aw;split => //; fprops. have fp: formulap x by apply:(formula_hi NS0); rewrite formulas_rec0. by split => //; apply/flength0P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)