;;; Proof for formula lists_or_trees.mc_flatten_app_flatten
;;; developed with old decision procedures
(""
 (AUTO-REWRITE "app" "flatten" "mc_flatten")
 (INDUCT "t")
 (("1" (SKOLEM * "e") (SKOLEM * "l") (GROUND))
  ("2"
   (SKOLEM * ("b1" "b2"))
   (FLATTEN)
   (SKOLEM * "l")
   (GROUND)
   (INST?)
   (INST?)
   (REPLACE - :HIDE? T)
   (REPLACE - :HIDE? T)
   (REWRITE "app_associative_proved_by_induction"))))

Note: if you wish to install this proof on the corresponding lemma in your PVS context, you can do it using Meta-x show-proof while the cursor is within the lemma (to display the proof buffer, normally empty), the copy the above proof to the proof buffer, and finally do Ctrl-x Ctrl-s to install the proof on your lemma, see PVS Emacs proof management commands.