Isabelle matters
change some definitions to be independent of the actual constructors,
eg change strIsFml to be an inductively defined set
Structform fml : strFmls, so as to make files independent of the actual syntax
in the proofs,
prove exclusion deletion terminating
approach transformation of tree one "step"
(ie one occurrence of Lemma 6) at a time
formalise FILL-validity