proposition: Lemma closed_increment: forall `{Lift T}, LiftLift -> forall k t, closed k t -> closed (1 + k) t.
proof: Proof. unfold closed. intros. match goal with h: shift _ _ = _ |- _ => rewrite <- h at 1 end. rewrite <- lift_lift by omega. congruence. Qed.
imports: Dblib.DblibTactics