proposition: Lemma enc_concat W s: AppL (Enc W) s ≡ enc (concat W) s.
proof: Proof. induction W; cbn; simplify; [auto..|]. now rewrite IHW. Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)