proposition: Lemma stack_eqb_spec : forall l1 l2, l1 = l2 <-> stack_eqb l1 l2 = true.
proof: Proof. intros l1 l2. unfold stack_eqb. destruct (list_eqb_spec (prod_eqb_spec (list_eqb_spec Bool.eqb_spec) (list_eqb_spec Bool.eqb_spec)) l1 l2); firstorder congruence. Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts ListEnumerabilityFacts) Lia Undecidability.L(LProd LBool LNat LOptions) Undecidability.L.Datatypes.List(List_basics List_eqb List_extra List_nat)