Hola.
La idea es probar el mismo lema pero usando la función inverse para generar el testigo en cada caso. Esto es, verificar que inverse satisface la especificación mirror.
Una opción es, al arrancar la prueba, dar como testigo (con exists) a inverse(t), y realizar la prueba en cada caso siguiendo la lógica de inverse.
Una alternativa (mejor) es usar la función inverse pera haciendo inducción funcional sobre ella:
Hint Constructors mirror.
Functional Scheme inverse_ind := Induction for inverse Sort Prop.
Lemma MirrorC : forall (A : Set) (t : bintree A), {t2 : bintree A | mirror A t t2}.
Proof.
intros A t; exists (inverse A t); functional induction inverse A t; auto.
Qed.
Saludos, Carlos