proposition: Lemma sub_dec (A B : list X) : (incl A B) + {x | x el A /\ ~ x el B}.
proof: Proof. Proof using HX. revert B. induction A; intros B; cbn; [left; apply incl_nil_l|]. destruct (IHA B); decide (a el B); auto. - left. now apply incl_cons. - right. exists a. split; auto. - destruct s as (x&H1&H2). right. exists x. split; auto. - right. exists a. split; auto. Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia