proposition: Lemma enc_cons b w s: enc (b :: w) s ≡ encb b (enc w s).
proof: Proof. unfold enc. eapply equiv_join. { now rewrite stepBeta. } rewrite stepBeta; [|reflexivity]. asimpl. rewrite map_map, map_id_list. rewrite map_map, map_id_list. eauto. all: intros; now asimpl. Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)