proposition: Lemma map_lift_map_lift: forall T k s wk ws (e : env T), forall `{Lift T}, @LiftLift T _ -> k <= s -> map (lift wk k) (map (lift ws s) e) = map (lift ws (wk + s)) (map (lift wk k) e).
proof: Proof. eauto using map_map_exchange, @lift_lift. Qed.
imports: List Dblib(DblibTactics DeBruijn)