proposition: Lemma enc_nil s: enc [] s ≡ s.
proof: Proof. unfold enc; cbn. rewrite stepBeta; asimpl; cbn; (eauto 2). Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)