proposition: Lemma wf_efree i n ts : all (wf i) ts -> all (wf i) (efree n ts).
proof: Proof. by elim: ts=>//= t ts IH; case: ifP=>_ /andP [] //= -> /IH ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)