proposition: Lemma enc_app w1 w2 s: enc (w1 ++ w2) s ≡ enc w1 (enc w2 s).
proof: Proof. induction w1; cbn; simplify; [auto..|]. now rewrite IHw1. Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)