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. unfold enc. intros H1 H2. cbn. f_equal. asimpl. f_equal. rewrite map_id_list; [auto..|]. intros x ?; mapinj; mapinj. asimpl. rewrite <-compComp_exp, encb_subst_id; (eauto 2). Qed.
imports: RelationClasses Morphisms List Lia Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus third_order.pcp)