Esta prueba la podés hacer usando la definición de well_founded (con unfold) primero y luego inducción en el árbol. Los subgoals salen usando constructor e inversion, esencialmente. También se podría usar Acc_intro, pero no es necesario.
Otra alternativa es usar una función como la cantidad de nodos para demostrar que un orden es bien fundado sobre árboles, llevando el problema al dominio de los naturales. Esto de hecho es lo que pide el ejercicio 8.
Require Import Wf_nat.
Require Import Inverse_Image.
Fixpoint size e :=
...
Definition elt e1 e2 := size e1 < size e2.
Theorem well_founded_elt : well_founded elt.
Proof.
apply (wf_inverse_image BoolExpr nat lt size).
...
Saludos, Carlos