proposition: Lemma permute_lift : forall M k, lift 1 (lift_rec 1 M k) = lift_rec 1 (lift 1 M) (S k).
proof: Proof. intros. change (lift_rec 1 (lift_rec 1 M k) 0 = lift_rec 1 (lift_rec 1 M 0) (1 + k)) in |- *. apply permute_lift_rec; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations