proposition: Lemma enc_eq w1 w2 s t: enc w1 s ≡ enc w2 t -> nostring s -> nostring t -> w1 = w2 /\ s ≡ t.
proof: Proof. Proof using u_neq_v. simplify. intros. induction w1 in w2, H |-*; destruct w2; cbn in *; (auto 2). - simplify in H; intuition easy. - simplify in H. destruct b; firstorder easy. - simplify in H; symmetry in H; destruct a; firstorder easy. - simplify in H; Injection H. eapply IHw1 in H3 as [-> ->]. now rewrite encb_eq with (a := a) (b := b). Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)