proposition: Lemma not_inclE (L L' : list X) : (not (incl L L')) -> { x | In x L /\ not (In x L')}.
proof: Proof. Proof using X_eq_dec. elim: L. { move=> H. exfalso. by apply: H. } move=> x L IH /=. have [|?] := In_dec X_eq_dec x L'. - move=> ? HxLL'. have /IH [y [? ?]] : ~ incl L L'. { move=> H. apply: HxLL'. by move=> y /= [<-|/H]. } exists y. tauto. - move=> _. exists x. tauto. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun