proposition: Lemma dec_enc s: { n | s = enc n} + forall n, s <> enc n.
proof: Proof. Proof with try (right; intros [] ?; discriminate). unfold enc. destruct s... destruct s... enough ({ n | s = AppL (repeat (var 0) n) (var 1)} + forall n, s <> AppL (repeat (var 0) n) (var 1)). - destruct H; [left|right]; intuition idtac. destruct s0 as [n]; exists n; now subst. injection H; eapply n; eauto. - induction s... + destruct f as [| []]... left; now (exists 0). + destruct s1 as [[] | | |]... destruct IHs2 as [[n IHs2]|IHs2]. * left. exists (S n). now subst. * right. intros []; try discriminate. cbn; injection 1; eapply IHs2. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)