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