proposition: Lemma encb_subst_id a (sigma: fin -> exp X): sigma u = var u -> sigma v = var v -> sigma • encb a = encb a.
proof: Proof. intros; unfold encb; cbn; destruct a; (eauto 2). Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)