proposition: Lemma encb_eq a b: encb a ≡ encb b -> a = b.
proof: Proof. Proof using u u_neq_v. intros H % equiv_head_equal; cbn in *; trivial. injection H; destruct a, b; intros; (eauto 1); exfalso; eapply u_neq_v; (eauto 2). Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)