proposition: Lemma Enc_subst_id (sigma: fin -> exp X) W: sigma u = var u -> sigma v = var v -> sigma •₊ Enc W = Enc W.
proof: Proof. intros. eapply map_id_list. intros; mapinj;eapply enc_subst_id; (eauto 2). Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)