proposition: Lemma enc_injective n m s t: isAtom s -> isAtom t -> enc n s ≡ enc m t -> n = m /\ s = t.
proof: Proof. induction n in m |-*; simplify in *; destruct m; simplify in *; intros. - intuition. destruct s, t; cbn in *; intuition; try Discriminate; Injection H1; congruence. - destruct s; cbn in *; intuition; Discriminate. - destruct t; cbn in *; intuition; Discriminate. - Injection H1. eapply IHn in H3; auto. intuition. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)