proposition: Lemma dec_enc: forall s, normal s -> { n | s a ≡ enc n a } + ({ n | s a ≡ enc n a } -> False).
proof: Proof. intros s N. specialize (@red_fun_rho _ (@step ag) (@par ag) rho) as f. do 4 mp f; try typeclasses eauto; auto. assert (s a ▷ rho (s a)). - eapply id in f as g. destruct g as [H1 H2]. split; [auto|]. destruct s; cbn. + eapply normal_app_intro; auto. + eapply normal_app_intro; auto. + eapply normal_subst. 1 - 2: intros []; cbn; auto. enough (rho s = s) as -> by auto using normal_lam_elim. eapply red_fun_fp; eauto using normal_lam_elim. + eapply head_atom in N as isA; [|auto]. assert (rho s1 = s1) as -> by (eapply red_fun_fp; eauto using normal_app_l, normal_app_r). assert (rho s2 = s2) as -> by (eapply red_fun_fp; eauto using normal_app_l, normal_app_r). destruct s1; cbn in isA; intuition. - destruct (dec_enc_eq (rho (s a))) as [[n H1]|H1]. + left. exists n. rewrite H1 in H. eapply equiv_join. rewrite H. all: auto. + right. intros [n H2]. eapply H1. exists n. eapply equiv_unique_normal_forms; auto. 2: eapply H. rewrite <-H2. symmetry. eapply equiv_join. rewrite H. all: auto. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)