Hola.
Mirando tus hipótesis, de H2 y H3 tendrías que x0 +++ x (o x +++ x0) debería ser nil. Con lo cual, tanto x0 como x deberían ser nil.
Luego, para probar propiedades que vinculen a append (+++) sugiero hacerlas aparte, como lemas auxiliares (con las hipótesis adecuadas).
Considerá:
Lemma list_append_nil : forall (A : Set) (l1 l2 : list A), l1 = l2 +++ l1 -> l2 = nil A.
Lemma list_append_nil2 : forall (A : Set) (l1 l2 : list A), l1 +++ l2 = nil A -> l1 = nil A /\ l2 = nil A.
El primer lema no es trivial. Si no te sale ponelo como axioma para completar la prueba.
Saludos, Carlos