proposition: Lemma dec_enc_eq : forall s, { n | s = enc n a } + ({ n | s = enc n a } -> False).
proof: Proof. induction s as [| [[[]|]|] | | s1 IH1 s3 IH3]. all: try (right; intros [[|n] ]; cbn; discriminate). - left. exists 0. reflexivity. - destruct IH3 as [[n]|]; subst. + destruct s1 as [| | | s1 s2 ]. all: try (right; intros [[|n'] ]; cbn; discriminate). destruct s1 as [| [[]|] | | ]. all: try (right; intros [[|n'] ]; cbn; discriminate). destruct s2 as [| [[]|] | | ]. all: try (right; intros [[|n'] ]; cbn; discriminate). left. exists (S n). reflexivity. + right. intros [n H]. destruct n; try discriminate; cbn in *; injection H. intros; eapply f; subst; now (exists n). Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)