tracking: proof checking

[c-cube]

Summarize progress in proof checking:

• update proof generation with renamings (or not), including rewrite
  steps and demod steps
• test this (without checking) on all TPTP; look for quick errors; merge into dev
• [ ] write LLTerm.t and basic functions (substitution/typing in particular)
• write simple CC based tableau (if possible, somehow incremental)
• conversion statement → formula
• make inference steps sth like
  intros [x,y,z]; apply C1 [g(y),x+1]; apply C2[z,z]; tableau
• skip some steps based on metadata (esa/arith) for now
• final summary on how many steps skipped/ok/fail
• debug on pure FO
• store result of checking inside proof steps
• direct β reduction of llterms
  ite/bool/β reduction rules in tableau
• make rewriting under λ terms pass proof checking
• proof checking for arith: FM / omega(?)/cooper
• proof check CNF steps, including tseitin
• proof check avatar (proof checking for avatar #64)
• lazy equality exchange (case split on all equalities between arith terms?)
• proof checking for full HO (proof checking for full HO #52)
• turn checking on by default
• fast proof checker (fast proof checker #53)