proposition: Lemma commut_lift_subst : forall M N k, subst_rec N (lift 1 M) (S k) = lift 1 (subst_rec N M k).
proof: Proof. intros; unfold lift in |- *. rewrite commut_lift_subst_rec; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations