proposition: Lemma list_eqb_spec A B : reflect (A = B) (list_eqb A B).
proof: Proof. Proof using spec. revert B; induction A; intros; destruct B; cbn in *; try now econstructor. destruct (spec a x), (IHA B); cbn; econstructor; congruence. Qed.
imports: Undecidability.L.Tactics(LTactics) Undecidability.L(Functions.EqBool)